[isabelle-dev] Isabelle cs. 70300f1b6835

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121020/5c19a815/attachment-0001.asc>