--- a/src/HOL/IsaMakefile Mon Aug 24 17:16:49 1998 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 24 18:17:25 1998 +0200
@@ -295,7 +295,8 @@
ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \
- ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML
+ ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
+ ex/Antiquote.thy ex/Antiquote.ML
@$(ISATOOL) usedir $(OUT)/HOL ex
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Antiquote.ML Mon Aug 24 18:17:25 1998 +0200
@@ -0,0 +1,11 @@
+
+Goal "P (EXPR (a + b + c))";
+Goal "P (EXPR (a + b + c + VAR x + VAR y + 1))";
+Goal "P (EXPR (VAR (f w) + VAR x))";
+
+Goal "P (Expr (%env. env))"; (*improper*)
+Goal "P (Expr (%env. f env))";
+Goal "P (Expr (%env. f env + env))"; (*improper*)
+Goal "P (Expr (%env. f env y z))";
+Goal "P (Expr (%env. f env + g y env))";
+Goal "P (Expr (%env. f env + g env y + h a env z))";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Antiquote.thy Mon Aug 24 18:17:25 1998 +0200
@@ -0,0 +1,27 @@
+(* Title: HOL/ex/Antiquote.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+
+Simple quote / antiquote example.
+*)
+
+Antiquote = Arith +
+
+syntax
+ "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
+
+constdefs
+ var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
+ "var x env == env x"
+
+ Expr :: "'a => 'a"
+ (*"(('a => nat) => nat) => (('a => nat) => nat)"*)
+ "Expr == (%x. x)"
+
+end
+
+
+ML
+
+val parse_translation = [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"];
+val print_translation = [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"];
--- a/src/HOL/ex/ROOT.ML Mon Aug 24 17:16:49 1998 +0200
+++ b/src/HOL/ex/ROOT.ML Mon Aug 24 18:17:25 1998 +0200
@@ -42,5 +42,8 @@
time_use_thy "PiSets";
time_use_thy "LocaleGroup";
+(*Expressions with quote / antiquote*)
+time_use_thy "Antiquote";
+
writeln "END: Root file for HOL examples";