equal
deleted
inserted
replaced
56 |
56 |
57 * Pure: dummy pattern "_" in is/let is now automatically lifted over |
57 * Pure: dummy pattern "_" in is/let is now automatically lifted over |
58 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") |
58 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") |
59 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x"); |
59 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x"); |
60 |
60 |
|
61 * Provers: 'simplified' attribute may refer to explicit rules instead |
|
62 of full simplifier context; 'iff' attribute handles conditional rules; |
|
63 |
61 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms; |
64 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms; |
62 |
65 |
63 * HOL: 'recdef' now fails on unfinished automated proofs, use |
66 * HOL: 'recdef' now fails on unfinished automated proofs, use |
64 "(permissive)" option to recover old behavior; |
67 "(permissive)" option to recover old behavior; |
65 |
68 |
96 |
99 |
97 - remove all special provisions on numerals in proofs; |
100 - remove all special provisions on numerals in proofs; |
98 |
101 |
99 * HOL/record: |
102 * HOL/record: |
100 - provides cases/induct rules for use with corresponding Isar methods; |
103 - provides cases/induct rules for use with corresponding Isar methods; |
101 - "record" operation truncates to particular fixed record (type cast); |
104 - old "make" and "make_scheme" operation removed -- INCOMPATIBILITY; |
102 - make_defs no longer part of default simps (INCOMPATIBILITY); |
105 - new derived operations "make" (for adding fields of current |
|
106 record), "extend" to promote fixed record to record scheme, and |
|
107 "truncate" for the reverse; cf. theorems "derived_defs", which are |
|
108 *not* declared as simp by default; |
103 - internal definitions directly based on a light-weight abstract |
109 - internal definitions directly based on a light-weight abstract |
104 theory of product types over typedef rather than datatype; |
110 theory of product types over typedef rather than datatype; |
105 |
111 |
106 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); |
112 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); |
107 |
113 |