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 