equal
deleted
inserted
replaced
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 