1.1 --- a/src/HOL/IsaMakefile	Thu Mar 23 10:23:54 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 23 11:27:52 2000 +0100
     1.3 @@ -425,7 +425,7 @@
     1.4    ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
     1.5    ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \
     1.6    ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
     1.7 -  ex/Antiquote.thy ex/Antiquote.ML ex/Points.thy
     1.8 +  ex/Antiquote.thy ex/Points.thy
     1.9  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.10  
    1.11  

     2.1 --- a/src/HOL/ex/Antiquote.ML	Thu Mar 23 10:23:54 2000 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,11 +0,0 @@
     2.4 -
     2.5 -Goal "P (EXPR (a + b + c))";
     2.6 -Goal "P (EXPR (a + b + c + VAR x + VAR y + 1))";
     2.7 -Goal "P (EXPR (VAR (f w) + VAR x))";
     2.8 -
     2.9 -Goal "P (Expr (%env. env))";				(*improper*)
    2.10 -Goal "P (Expr (%env. f env))";
    2.11 -Goal "P (Expr (%env. f env + env))";			(*improper*)
    2.12 -Goal "P (Expr (%env. f env y z))";
    2.13 -Goal "P (Expr (%env. f env + g y env))";
    2.14 -Goal "P (Expr (%env. f env + g env y + h a env z))";

     3.1 --- a/src/HOL/ex/Antiquote.thy	Thu Mar 23 10:23:54 2000 +0100
     3.2 +++ b/src/HOL/ex/Antiquote.thy	Thu Mar 23 11:27:52 2000 +0100
     3.3 @@ -5,23 +5,31 @@
     3.4  Simple quote / antiquote example.
     3.5  *)
     3.6  
     3.7 -Antiquote = Arith +
     3.8 +theory Antiquote = Main:;
     3.9  
    3.10  syntax
    3.11 -  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
    3.12 +  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999);
    3.13  
    3.14  constdefs
    3.15    var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
    3.16    "var x env == env x"
    3.17  
    3.18 -  Expr :: "'a => 'a"
    3.19 -	(*"(('a => nat) => nat) => (('a => nat) => nat)"*)
    3.20 -  "Expr == (%x. x)"
    3.21 +  Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
    3.22 +  "Expr exp env == exp env";
    3.23  
    3.24 -end
    3.25 +parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *};
    3.26 +print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *};
    3.27  
    3.28 +term "EXPR (a + b + c)";
    3.29 +term "EXPR (a + b + c + VAR x + VAR y + 1)";
    3.30 +term "EXPR (VAR (f w) + VAR x)";
    3.31  
    3.32 -ML
    3.33 +term "Expr (%env. env x)";				(*improper*)
    3.34 +term "Expr (%env. f env)";
    3.35 +term "Expr (%env. f env + env x)";			(*improper*)
    3.36 +term "Expr (%env. f env y z)";
    3.37 +term "Expr (%env. f env + g y env)";
    3.38 +term "Expr (%env. f env + g env y + h a env z)";
    3.39  
    3.40 -val parse_translation = [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"];
    3.41 -val print_translation = [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"];
    3.42 +end;
    3.43 +