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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
