equal
deleted
inserted
replaced
78 * HOL/record: fixed select-update simplification procedure to handle |
78 * HOL/record: fixed select-update simplification procedure to handle |
79 extended records as well; admit "r" as field name; |
79 extended records as well; admit "r" as field name; |
80 |
80 |
81 * HOL/ex: new theory Factorization proving the Fundamental Theorem of |
81 * HOL/ex: new theory Factorization proving the Fundamental Theorem of |
82 Arithmetic, by Thomas M Rasmussen; |
82 Arithmetic, by Thomas M Rasmussen; |
|
83 |
|
84 * HOL/ex/Multiquote: multiple nested quotations and anti-quotations -- |
|
85 basically a generalized version of de-Bruijn representation; very |
|
86 useful in avoiding lifting all operations; |
83 |
87 |
84 * new version of "case_tac" subsumes both boolean case split and |
88 * new version of "case_tac" subsumes both boolean case split and |
85 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
89 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
86 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
90 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
87 |
91 |