HOL/ex/Multiquote;
authorwenzelm
Fri, 24 Mar 2000 17:29:51 +0100
changeset 857063d4f3ea2e70
parent 8569 748a9699f28d
child 8571 c323613e4a47
HOL/ex/Multiquote;
NEWS
     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;