[isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31

[Andrei Popescu]

Makarius wrote: 


>> Can you explain the squiggle =: above?  I did not find it in the manual
>> nor in the sources so far.  It seems to be special to main HOL datatypes.


I had not even noticed that weird-looking combination of symbols.    :-)

Now I see that what it does is indicate for Nil that a discriminator (of type "'a list => bool") 

should not be provided, but instead equality with Nil should be used.  

This option seems to only be available for nullary constructors.  


Andrei