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

[Florian Haftmann]

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.

Cheers,
	Florian

-------------- 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>