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

[Makarius]

On Sat, 24 May 2014, Andrei Popescu wrote:

>>> (1) Its definition looks terrific:
>
>>> datatype_new (set: 'a) list (map: map rel: list_all2) =
>>>    =: Nil (defaults tl: "[]")  ("[]")
>>>   | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
>
> By all "means" terrific.  :-) 
> From Merriam-Webster dictionary, terrific can mean: 
>
> 1: frightful 
> 2: unusually fine

Indeed.

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.


 	Makarius