equal
deleted
inserted
replaced
117 |
117 |
118 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
118 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
119 -- avoids syntactic ambiguities and treats state, transition, and |
119 -- avoids syntactic ambiguities and treats state, transition, and |
120 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
120 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
121 changed syntax and (many) tactics; |
121 changed syntax and (many) tactics; |
|
122 |
|
123 * HOL/datatype: Now also handles arbitrarily branching datatypes |
|
124 (using function types) such as |
|
125 |
|
126 datatype 'a tree = Atom 'a | Branch "nat => 'a tree" |
122 |
127 |
123 * HOL/typedef: fixed type inference for representing set; type |
128 * HOL/typedef: fixed type inference for representing set; type |
124 arguments now have to occur explicitly on the rhs as type constraints; |
129 arguments now have to occur explicitly on the rhs as type constraints; |
125 |
130 |
126 * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects |
131 * HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects |