[isabelle-dev] A suggestion: call eval with try0

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Mon Aug 17 19:27:45 CEST 2020

Am 17.08.20 um 13:39 schrieb Manuel Eberl:
> Yes, that's called code_simp.
> The difference, however, is often several orders of magnitude, which
> makes code_simp unfeasible in most cases.
> I always wondered /why/ it is that slow and whether this is just not
> optimised that well or whether it's some unavoidable bottleneck.

There is e.g. no proper counter part for abstract data types.  Nowadays
I would not consider code_simp a serious business any longer.

Btw. this discussion would fit in scope to the Isabelle user mailing list.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200817/107e7cd5/attachment-0001.sig>

More information about the isabelle-dev mailing list