1.1 --- a/src/HOL/IsaMakefile	Mon Aug 24 17:16:49 1998 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Aug 24 18:17:25 1998 +0200
     1.3 @@ -295,7 +295,8 @@
     1.4    ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
     1.5    ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
     1.6    ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \
     1.7 -  ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML
     1.8 +  ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
     1.9 +  ex/Antiquote.thy ex/Antiquote.ML
    1.10  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.11  
    1.12  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Antiquote.ML	Mon Aug 24 18:17:25 1998 +0200
     2.3 @@ -0,0 +1,11 @@
     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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Antiquote.thy	Mon Aug 24 18:17:25 1998 +0200
     3.3 @@ -0,0 +1,27 @@
     3.4 +(*  Title:      HOL/ex/Antiquote.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +
     3.8 +Simple quote / antiquote example.
     3.9 +*)
    3.10 +
    3.11 +Antiquote = Arith +
    3.12 +
    3.13 +syntax
    3.14 +  "_Expr" :: "'a => 'a"				("EXPR _" [1000] 999)
    3.15 +
    3.16 +constdefs
    3.17 +  var :: "'a => ('a => nat) => nat"		("VAR _" [1000] 999)
    3.18 +  "var x env == env x"
    3.19 +
    3.20 +  Expr :: "'a => 'a"
    3.21 +	(*"(('a => nat) => nat) => (('a => nat) => nat)"*)
    3.22 +  "Expr == (%x. x)"
    3.23 +
    3.24 +end
    3.25 +
    3.26 +
    3.27 +ML
    3.28 +
    3.29 +val parse_translation = [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"];
    3.30 +val print_translation = [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"];

     4.1 --- a/src/HOL/ex/ROOT.ML	Mon Aug 24 17:16:49 1998 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Mon Aug 24 18:17:25 1998 +0200
     4.3 @@ -42,5 +42,8 @@
     4.4  time_use_thy "PiSets";
     4.5  time_use_thy "LocaleGroup";
     4.6  
     4.7 +(*Expressions with quote / antiquote*)
     4.8 +time_use_thy "Antiquote";
     4.9 +
    4.10  
    4.11  writeln "END: Root file for HOL examples";