NEWS
changeset 7047 d103b875ef1d
parent 6925 8d4d45ec6a3d
child 7113 ab79d9fa8d8e
equal deleted inserted replaced
7046:9f755ff43cff 7047:d103b875ef1d
   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