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



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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