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

[Andrei Popescu]

Hi Makarius, 


>> (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

These items that the user traditionally takes the trouble to define "by hand" are now provided 

for free for any (co)datatype: the selectors and discriminators, the set function, the relator.  

These names that seem to clutter the specification are entirely optional -- if not specified, 

default names are produced.    


You of course know all these, but I wanted to take this opportunity to reiterate the advances 

of the new (co)datatype.  


Cheers, 

  Andrei