equal
deleted
inserted
replaced
150 including theory commands '(co)inductive', '(co)datatype', |
150 including theory commands '(co)inductive', '(co)datatype', |
151 'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', |
151 'rep_datatype', 'inductive_cases', as well as methods 'ind_cases', |
152 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); |
152 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC'); |
153 |
153 |
154 |
154 |
155 |
|
156 *** HOL *** |
155 *** HOL *** |
157 |
156 |
158 * HOL: moved over to sane numeral syntax; the new policy is as |
157 * HOL: moved over to sane numeral syntax; the new policy is as |
159 follows: |
158 follows: |
160 |
159 |
226 necessary to attach explicit type constraints; |
225 necessary to attach explicit type constraints; |
227 |
226 |
228 * HOL: syntax translations now work properly with numerals and records |
227 * HOL: syntax translations now work properly with numerals and records |
229 expressions; |
228 expressions; |
230 |
229 |
231 * HOL/GroupTheory: group theory examples including Sylow's theorem, by |
230 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead |
232 Florian Kammüller; |
231 of "lam" -- INCOMPATIBILITY; |
233 |
232 |
234 * HOL: got rid of some global declarations (potential INCOMPATIBILITY |
233 * HOL: got rid of some global declarations (potential INCOMPATIBILITY |
235 for ML tools): const "()" renamed "Product_Type.Unity", type "unit" |
234 for ML tools): const "()" renamed "Product_Type.Unity", type "unit" |
236 renamed "Product_Type.unit"; |
235 renamed "Product_Type.unit"; |
|
236 |
|
237 * HOL/GroupTheory: group theory examples including Sylow's theorem, by |
|
238 Florian Kammüller; |
237 |
239 |
238 |
240 |
239 *** HOLCF *** |
241 *** HOLCF *** |
240 |
242 |
241 * proper rep_datatype lift (see theory Lift) instead of ML hacks -- |
243 * proper rep_datatype lift (see theory Lift) instead of ML hacks -- |