equal
deleted
inserted
replaced
49 * Pure: renamed "antecedent" case to "rule_context"; |
49 * Pure: renamed "antecedent" case to "rule_context"; |
50 |
50 |
51 * Pure: added 'corollary' command; |
51 * Pure: added 'corollary' command; |
52 |
52 |
53 * Pure: fixed 'token_translation' command; |
53 * Pure: fixed 'token_translation' command; |
|
54 |
|
55 * Pure: removed obsolete 'exported' attribute; |
|
56 |
|
57 * Pure: dummy pattern "_" in is/let is now automatically ``lifted'' |
|
58 over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") |
|
59 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x"); |
54 |
60 |
55 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms; |
61 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms; |
56 |
62 |
57 * HOL: 'recdef' now fails on unfinished automated proofs, use |
63 * HOL: 'recdef' now fails on unfinished automated proofs, use |
58 "(permissive)" option to recover old behavior; |
64 "(permissive)" option to recover old behavior; |