Re: [isabelle] New AFP theory: List Index



On Sun, 21 Feb 2010, Brian Huffman wrote:

Of course, I can always define nice syntax to use within the library
itself, and then use "no_syntax" at the end to avoid potential clashes
with user theories.

Better use 'notation' / 'no_notation' which perform static checking of the term constants involved. The more primitive 'syntax' / 'no_syntax' is only needed for very special syntax table manipulations.


	Makarius






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