NEWS
changeset 3227 9190438471ea
parent 3205 816a1f9fd620
child 3316 c2e9ab7d2724
equal deleted inserted replaced
3226:04618aca579d 3227:9190438471ea
   103 harmonize with FOL, ZF, LK, etc.;
   103 harmonize with FOL, ZF, LK, etc.;
   104 
   104 
   105 * HOL/ex/LFilter theory of a corecursive "filter" functional for
   105 * HOL/ex/LFilter theory of a corecursive "filter" functional for
   106 infinite lists;
   106 infinite lists;
   107 
   107 
       
   108 * HOL/Modelcheck demonstrates invocation of model checker oracle;
       
   109 
   108 * HOL/ex/Ring.thy declares cring_simp, which solves equational
   110 * HOL/ex/Ring.thy declares cring_simp, which solves equational
   109 problems in commutative rings, using axiomatic type classes for + and *;
   111 problems in commutative rings, using axiomatic type classes for + and *;
   110 
   112 
   111 * more examples in HOL/MiniML and HOL/Auth;
   113 * more examples in HOL/MiniML and HOL/Auth;
   112 
   114