equal
deleted
inserted
replaced
188 * HOL/record package improvements: |
188 * HOL/record package improvements: |
189 - new derived operations "fields" to build a partial record section, |
189 - new derived operations "fields" to build a partial record section, |
190 "extend" to promote a fixed record to a record scheme, and |
190 "extend" to promote a fixed record to a record scheme, and |
191 "truncate" for the reverse; cf. theorems "xxx.defs", which are *not* |
191 "truncate" for the reverse; cf. theorems "xxx.defs", which are *not* |
192 declared as simp by default; |
192 declared as simp by default; |
|
193 - shared operations ("more", "fields", etc.) now need to be always |
|
194 qualified) --- potential INCOMPATIBILITY; |
193 - removed "make_scheme" operations (use "make" with "extend") -- |
195 - removed "make_scheme" operations (use "make" with "extend") -- |
194 INCOMPATIBILITY; |
196 INCOMPATIBILITY; |
195 - removed "more" class (simply use "term") -- INCOMPATIBILITY; |
197 - removed "more" class (simply use "term") -- INCOMPATIBILITY; |
196 - provides cases/induct rules for use with corresponding Isar |
198 - provides cases/induct rules for use with corresponding Isar |
197 methods (for concrete records, record schemes, concrete more |
199 methods (for concrete records, record schemes, concrete more |