Hi Ondrej, the changeset http://isabelle.in.tum.de/reports/Isabelle/rev/70300f1b6835 broke the AFP sessions JinjaThreads and KBPs.
After having a closer look at it, I would suggest two things:
a) Keeping lemmas lookup_Mapping, Mapping_lookup, Mapping_inject,
mapping_eq_iff, mapping_eqI since they are really fundamental and help
in cases where transfer fails.
b) Try hard to eliminate »rep« again and replace it by »lookup«. This
is plain cloning, an this is really bad. What happens if you substitute
»lookup« for »rep« in the typedef and drop the separate definition for
»lookup«? Maybe it goes through without further ado.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
