Hol_datatype : hol_type quotation -> unit
STRUCTURE
bossLib
SYNOPSIS
Define a concrete datatype (deprecated syntax).
DESCRIPTION
The Hol_datatype function provides exactly the same definitional power as the Datatype function (which see), with a slightly different input syntax, given below: 
   spec    ::= [ <binding> ; ]* <binding>

   binding ::= <ident> = [ <clause> | ]* <clause>
            |  <ident> = <| [ <ident> : <type> ; ]* <ident> : <type> |>

   clause  ::= <ident>
            |  <ident> of [<type> => ]* <type>
EXAMPLE
For example, what with Datatype would be 
   Datatype`btree = Leaf 'a | Node btree 'b btree
is 
   Hol_datatype `btree = Leaf of 'a
                       | Node of btree => 'b => btree`
when using Hol_datatype.

The => notation in the description highlights the fact that, in HOL, constructors are by default curried.

COMMENTS
The Datatype function’s syntax is easier to write and easier to understand.
SEEALSO
Datatype
HOL  Kananaskis-14