equal
deleted
inserted
replaced
117 |
117 |
118 * more examples in HOL/MiniML and HOL/Auth; |
118 * more examples in HOL/MiniML and HOL/Auth; |
119 |
119 |
120 * more default rewrite rules for quantifiers, union/intersection; |
120 * more default rewrite rules for quantifiers, union/intersection; |
121 |
121 |
|
122 * a new constant `arbitrary == @x.False'; |
|
123 |
122 * HOLCF/IOA replaces old HOL/IOA; |
124 * HOLCF/IOA replaces old HOL/IOA; |
123 |
125 |
124 * HOLCF changes: derived all rules and arities |
126 * HOLCF changes: derived all rules and arities |
125 + axiomatic type classes instead of classes |
127 + axiomatic type classes instead of classes |
126 + typedef instead of faking type definitions |
128 + typedef instead of faking type definitions |