#
de2ed6a8 |
|
10-Dec-1999 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Changes due to the incorporation of John Harrison's datatype definition package. Here are the rest of the significant changes. The interface in Datatype has been fleshed out quite a bit, but what was there has stayed pretty much the same (except that prim_Hol_datatype doesn't write stuff out to disk anymore; it's hardly very pure if it does so). The ind_type theory is the basis for ind_types, which is in turn called from Datatype.
|