# HG changeset patch
# User wenzelm
# Date 953915391 -3600
# Node ID 63d4f3ea2e708950e0bb2fd3cd9d904023340f74
# Parent  748a9699f28d392a2fba7b9f021cf80d03de2a5e
HOL/ex/Multiquote;

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