equal
deleted
inserted
replaced
289 |
289 |
290 * Inductive package: offers new command "inductive_simps" to automatically |
290 * Inductive package: offers new command "inductive_simps" to automatically |
291 derive instantiated and simplified equations for inductive predicates, |
291 derive instantiated and simplified equations for inductive predicates, |
292 similar to inductive_cases. |
292 similar to inductive_cases. |
293 |
293 |
294 * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a |
294 * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an |
295 generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV". |
295 abbreviation of "range f = UIV". The theorems bij_def and surj_def are |
296 The theorems bij_def and surj_def are unchanged. |
296 unchanged. |
|
297 INCOMPATIBILITY. |
297 |
298 |
298 * Function package: .psimps rules are no longer implicitly declared [simp]. |
299 * Function package: .psimps rules are no longer implicitly declared [simp]. |
299 INCOMPATIBILITY. |
300 INCOMPATIBILITY. |
300 |
301 |
301 * Weaker versions of the "meson" and "metis" proof methods are now available in |
302 * Weaker versions of the "meson" and "metis" proof methods are now available in |