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