1.1 --- a/src/HOL/IsaMakefile	Fri Mar 24 14:40:51 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Mar 24 17:28:03 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/Points.thy
     1.8 +  ex/Antiquote.thy ex/Multiquote.thy ex/Points.thy
     1.9  	@$(ISATOOL) usedir $(OUT)/HOL ex
    1.10  
    1.11  

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Multiquote.thy	Fri Mar 24 17:28:03 2000 +0100
     2.3 @@ -0,0 +1,45 @@
     2.4 +(*  Title:      HOL/ex/Multiquote.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Markus Wenzel, TU Muenchen
     2.7 +
     2.8 +Multiple nested quotations and anti-quotations -- basically a
     2.9 +generalized version of de-Bruijn representation.
    2.10 +*)
    2.11 +
    2.12 +theory Multiquote = Main:;
    2.13 +
    2.14 +syntax
    2.15 +  "_quote" :: "'b \\<Rightarrow> ('a \\<Rightarrow> 'b)"	     ("{._.}" [0] 1000)
    2.16 +  "_antiquote" :: "('a \\<Rightarrow> 'b) \\<Rightarrow> 'b"        ("`_" [1000] 999);
    2.17 +
    2.18 +parse_translation {*
    2.19 +  let
    2.20 +    fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
    2.21 +          skip_antiquote_tr i t
    2.22 +      | antiquote_tr i (Const ("_antiquote", _) $ t) =
    2.23 +          antiquote_tr i t $ Bound i
    2.24 +      | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
    2.25 +      | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
    2.26 +      | antiquote_tr _ a = a
    2.27 +    and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
    2.28 +          c $ skip_antiquote_tr i t
    2.29 +      | skip_antiquote_tr i t = antiquote_tr i t;
    2.30 +
    2.31 +    fun quote_tr [t] = Abs ("state", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    2.32 +      | quote_tr ts = raise TERM ("quote_tr", ts);
    2.33 +  in [("_quote", quote_tr)] end
    2.34 +*};
    2.35 +
    2.36 +text {* basic examples *};
    2.37 +term "{. a + b + c .}";
    2.38 +term "{. a + b + c + `x + `y + 1 .}";
    2.39 +term "{. `(f w) + `x .}";
    2.40 +term "{. f (`x) (`y) z .}";
    2.41 +
    2.42 +text {* advanced examples *};
    2.43 +term "{. {. `(`x) + `y .} .}";
    2.44 +term "{. {. `(`x) + `y .} o `f .}";
    2.45 +term "{. `(f o `g) .}";
    2.46 +term "{. {. `(`(f o `g)) .} .}";
    2.47 +
    2.48 +end;

     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Mar 24 14:40:51 2000 +0100
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Mar 24 17:28:03 2000 +0100
     3.3 @@ -48,6 +48,7 @@
     3.4  
     3.5  (*expressions with quote / antiquote syntax*)
     3.6  time_use_thy "Antiquote";
     3.7 +time_use_thy "Multiquote";
     3.8  
     3.9  
    3.10  writeln "END: Root file for HOL examples";