[isabelle-dev] isabelle-dev Digest, Vol 84, Issue 31
uuomul at yahoo.com
Sat May 24 20:25:56 CEST 2014
>> 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.
More information about the isabelle-dev