equal
deleted
inserted
replaced
233 similar to inductive_cases. |
233 similar to inductive_cases. |
234 |
234 |
235 * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a |
235 * "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a |
236 generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV". |
236 generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV". |
237 The theorems bij_def and surj_def are unchanged. |
237 The theorems bij_def and surj_def are unchanged. |
|
238 |
|
239 * Function package: .psimps rules are no longer implicitly declared [simp]. |
|
240 INCOMPATIBILITY. |
238 |
241 |
239 *** FOL *** |
242 *** FOL *** |
240 |
243 |
241 * All constant names are now qualified. INCOMPATIBILITY. |
244 * All constant names are now qualified. INCOMPATIBILITY. |
242 |
245 |