[isabelle-dev] Isabelle cs. 70300f1b6835
florian.haftmann at informatik.tu-muenchen.de
Sun Oct 21 16:42:25 CEST 2012
> 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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 259 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev