[isabelle-dev] Unqualified swap?

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sat Apr 12 19:02:35 CEST 2014


In 8f1e7596deb7 I have introduced

	swap :: 'a * 'b => 'b * 'a

on products.

Is this common enough to be left unqualified?  I hesitated to qualify it
since Product_Type.swap is too cumbersome (although something different
could be achieved using low-level namespace manipulation).

(One might ask whether the _Type suffix on Product_Type.thy (and Sum.thy
and some others in Library/) should be discontinued then, but this is
another question)

Any remarks?
	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: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140412/b449c78d/attachment.asc>


More information about the isabelle-dev mailing list