127 -- "now uniform 'a::bar instead of default sort for first occurrence (!)" |
127 -- "now uniform 'a::bar instead of default sort for first occurrence (!)" |
128 |
128 |
129 |
129 |
130 *** HOL *** |
130 *** HOL *** |
131 |
131 |
132 |
|
133 * New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove"). |
132 * New tutorial "Programming and Proving in Isabelle/HOL" ("prog-prove"). |
134 It completely supercedes "A Tutorial Introduction to Structured Isar Proofs", |
133 It completely supercedes "A Tutorial Introduction to Structured Isar Proofs", |
135 which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant |
134 which has been removed. It supercedes "Isabelle/HOL, A Proof Assistant |
136 for Higher-Order Logic" as the recommended beginners tutorial |
135 for Higher-Order Logic" as the recommended beginners tutorial |
137 but does not cover all of the material of that old tutorial. |
136 but does not cover all of the material of that old tutorial. |
138 |
137 |
139 * Discontinued old Tutorial on Isar ("isar-overview"); |
138 * Discontinued old Tutorial on Isar ("isar-overview"); |
140 |
|
141 * The representation of numerals has changed. We now have a datatype |
|
142 "num" representing strictly positive binary numerals, along with |
|
143 functions "numeral :: num => 'a" and "neg_numeral :: num => 'a" to |
|
144 represent positive and negated numeric literals, respectively. (See |
|
145 definitions in Num.thy.) Potential INCOMPATIBILITY; some user theories |
|
146 may require adaptations: |
|
147 |
|
148 - Theorems with number_ring or number_semiring constraints: These |
|
149 classes are gone; use comm_ring_1 or comm_semiring_1 instead. |
|
150 |
|
151 - Theories defining numeric types: Remove number, number_semiring, |
|
152 and number_ring instances. Defer all theorems about numerals until |
|
153 after classes one and semigroup_add have been instantiated. |
|
154 |
|
155 - Numeral-only simp rules: Replace each rule having a "number_of v" |
|
156 pattern with two copies, one for numeral and one for neg_numeral. |
|
157 |
|
158 - Theorems about subclasses of semiring_1 or ring_1: These classes |
|
159 automatically support numerals now, so more simp rules and |
|
160 simprocs may now apply within the proof. |
|
161 |
|
162 - Definitions and theorems using old constructors Pls/Min/Bit0/Bit1: |
|
163 Redefine using other integer operations. |
|
164 |
139 |
165 * Type 'a set is now a proper type constructor (just as before |
140 * Type 'a set is now a proper type constructor (just as before |
166 Isabelle2008). Definitions mem_def and Collect_def have disappeared. |
141 Isabelle2008). Definitions mem_def and Collect_def have disappeared. |
167 Non-trivial INCOMPATIBILITY. For developments keeping predicates and |
142 Non-trivial INCOMPATIBILITY. For developments keeping predicates and |
168 sets separate, it is often sufficient to rephrase sets S accidentally |
143 sets separate, it is often sufficient to rephrase sets S accidentally |