equal
deleted
inserted
replaced
163 * New method "linarith" invokes existing linear arithmetic decision |
163 * New method "linarith" invokes existing linear arithmetic decision |
164 procedure only. |
164 procedure only. |
165 |
165 |
166 * New implementation of quickcheck uses generic code generator; |
166 * New implementation of quickcheck uses generic code generator; |
167 default generators are provided for all suitable HOL types, records |
167 default generators are provided for all suitable HOL types, records |
168 and datatypes. |
168 and datatypes. Old quickcheck can be re-activated importing |
|
169 theory Library/SML_Quickcheck. |
169 |
170 |
170 * Renamed theorems: |
171 * Renamed theorems: |
171 Suc_eq_add_numeral_1 -> Suc_eq_plus1 |
172 Suc_eq_add_numeral_1 -> Suc_eq_plus1 |
172 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left |
173 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left |
173 Suc_plus1 -> Suc_eq_plus1 |
174 Suc_plus1 -> Suc_eq_plus1 |