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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
