equal
deleted
inserted
replaced
120 |
120 |
121 page 256,258: list_case now takes the list as its last argument, not the |
121 page 256,258: list_case now takes the list as its last argument, not the |
122 first. |
122 first. |
123 |
123 |
124 page 259: HOL theory files may now include datatype declarations, primitive |
124 page 259: HOL theory files may now include datatype declarations, primitive |
125 recursive function definitions, and (co)inductive definitions. (These new |
125 recursive function definitions, and (co)inductive definitions. These new |
126 sections are available separately as the file ml/HOL-extensions.dvi.gz, |
126 sections are available separately at |
127 host ftp.cl.cam.ac.uk.) |
127 http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOL-extensions.dvi.gz |
128 |
128 |
129 page 259: now there is another examples directory, IMP (a semantics |
129 page 259: now there is another examples directory, IMP (a semantics |
130 equivalence proof for an imperative language) |
130 equivalence proof for an imperative language) |