NEWS
changeset 12177 b1c16d685a99
parent 12163 04c98351f9af
child 12210 2f510d8d8291
equal deleted inserted replaced
12176:f9139e09a983 12177:b1c16d685a99
   207 HOLCF/ex/Dnat.thy;
   207 HOLCF/ex/Dnat.thy;
   208 
   208 
   209 
   209 
   210 *** ZF ***
   210 *** ZF ***
   211 
   211 
       
   212 * ZF: new-style theory commands 'inductive', 'inductive_cases', and
       
   213 methods 'ind_cases', 'induct_tac', 'case_tac';
       
   214 
   212 * ZF: the integer library now covers quotients and remainders, with
   215 * ZF: the integer library now covers quotients and remainders, with
   213 many laws relating division to addition, multiplication, etc.;
   216 many laws relating division to addition, multiplication, etc.;
   214 
   217 
   215 * ZF/Induct: new directory for examples of inductive definitions, including theory
   218 * ZF/Induct: new directory for examples of inductive definitions,
   216 Multiset for multiset orderings;
   219 including theory Multiset for multiset orderings;
   217 
   220 
   218 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless
   221 * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
   219 version of the formalism;
   222 typeless version of the formalism;
   220 
   223 
   221 
   224 
   222 *** General ***
   225 *** General ***
   223 
   226 
   224 * kernel: meta-level proof terms (by Stefan Berghofer), see also ref
   227 * kernel: meta-level proof terms (by Stefan Berghofer), see also ref