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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and