[isabelle-dev] Isabelle cs. 70300f1b6835

[Florian Haftmann]

Hi Ondrej,

> But your observation gave me an idea that actually I should remove the
> explicit names for morphisms in Mapping.thy completely and then you
> wouldn't even notice there are any abstraction and representation
> functions behind the scene.

I would conclude that if abs and rep are completely opaque and do not
appear in user space (cf. find_theorems!), the duplication lookup == rep
is fine.

Concerning the transfer-or-not question, the mapping type is not really
an issue and I don't really mind loosing mapping_eq_iff etc.  However
there are types where transfer is not the only valid approach to conduct
proofs on, e.g. multisets, as far as I can forsee at the moment.  So it
would be too much rush to drop all those fundamental lemmas there.
Maybe future will bring more insight on this.

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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121021/677bf01f/attachment.sig>