# HG changeset patch
# User wenzelm
# Date 903975445 -7200
# Node ID 7c8d1c7c876dcae345cc143484a7143efe6720cc
# Parent  33f81e980c938bb42409b816153d77e74ef21f2d
added Antiquote example;

diff -r 33f81e980c93 -r 7c8d1c7c876d src/HOL/IsaMakefile
--- 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
 
 
diff -r 33f81e980c93 -r 7c8d1c7c876d src/HOL/ex/Antiquote.ML
--- /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))";
diff -r 33f81e980c93 -r 7c8d1c7c876d src/HOL/ex/Antiquote.thy
--- /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"];
diff -r 33f81e980c93 -r 7c8d1c7c876d src/HOL/ex/ROOT.ML
--- 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";