# HG changeset patch
# User wenzelm
# Date 953807272 -3600
# Node ID fd37531882325c245e84b278110587607e776046
# Parent  6c4860b1828dd0a408e024a7d0d4774432f5d5a1
ex/Antiquote.thy made new-style theory;
removed ex/Antiquote.ML;

diff -r 6c4860b1828d -r fd3753188232 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 23 10:23:54 2000 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 23 11:27:52 2000 +0100
@@ -425,7 +425,7 @@
   ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
   ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \
   ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
-  ex/Antiquote.thy ex/Antiquote.ML ex/Points.thy
+  ex/Antiquote.thy ex/Points.thy
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 
diff -r 6c4860b1828d -r fd3753188232 src/HOL/ex/Antiquote.ML
--- a/src/HOL/ex/Antiquote.ML	Thu Mar 23 10:23:54 2000 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-
-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 6c4860b1828d -r fd3753188232 src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Thu Mar 23 10:23:54 2000 +0100
+++ b/src/HOL/ex/Antiquote.thy	Thu Mar 23 11:27:52 2000 +0100
@@ -5,23 +5,31 @@
 Simple quote / antiquote example.
 *)
 
-Antiquote = Arith +
+theory Antiquote = Main:;
 
 syntax
-  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
+  "_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)"
+  Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
+  "Expr exp env == exp env";
 
-end
+parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *};
+print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *};
+
+term "EXPR (a + b + c)";
+term "EXPR (a + b + c + VAR x + VAR y + 1)";
+term "EXPR (VAR (f w) + VAR x)";
 
-
-ML
+term "Expr (%env. env x)";				(*improper*)
+term "Expr (%env. f env)";
+term "Expr (%env. f env + env x)";			(*improper*)
+term "Expr (%env. f env y z)";
+term "Expr (%env. f env + g y env)";
+term "Expr (%env. f env + g env y + h a env z)";
 
-val parse_translation = [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"];
-val print_translation = [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"];
+end;
+