Re: [isabelle] disabling datatype syntax



Hi Chris,

the easiest way to tinker around with constant syntax nowadays is the
notation / no_notation mechanism, as in the following example:

	datatype foo = Bla
	term Bla

	notation Bla ("Blubb")
	term Bla

	no_notation Bla ("Blubb")
	term Bla

Note that the arguments to no_notation have to match the corresponding
notation declaration exactly.

For more refer to the Isabelle Reference Manual.

Hope this helps
	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.