1.1 --- a/NEWS Fri Mar 24 17:28:03 2000 +0100
1.2 +++ b/NEWS Fri Mar 24 17:29:51 2000 +0100
1.3 @@ -81,6 +81,10 @@
1.4 * HOL/ex: new theory Factorization proving the Fundamental Theorem of
1.5 Arithmetic, by Thomas M Rasmussen;
1.6
1.7 +* HOL/ex/Multiquote: multiple nested quotations and anti-quotations --
1.8 +basically a generalized version of de-Bruijn representation; very
1.9 +useful in avoiding lifting all operations;
1.10 +
1.11 * new version of "case_tac" subsumes both boolean case split and
1.12 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
1.13 exists, may define val exhaust_tac = case_tac for ad-hoc portability;