src/HOL/ex/Multiquote.thy
changeset 8578 3b9e3c782eb2
parent 8572 794843a9d8b1
child 8627 44ec33bb5c5b
     1.1 --- a/src/HOL/ex/Multiquote.thy	Sat Mar 25 17:59:52 2000 +0100
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Sat Mar 25 18:01:27 2000 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  theory Multiquote = Main:;
     1.5  
     1.6  syntax
     1.7 -  "_quote" :: "'b => ('a => 'b)"	     ("{._.}" [0] 1000)
     1.8 -  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 999);
     1.9 +  "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
    1.10 +  "_antiquote" :: "('a => 'b) => 'b"         ("`_" [1000] 1000);
    1.11  
    1.12  parse_translation {*
    1.13    let
    1.14 @@ -25,21 +25,21 @@
    1.15            c $ skip_antiquote_tr i t
    1.16        | skip_antiquote_tr i t = antiquote_tr i t;
    1.17  
    1.18 -    fun quote_tr [t] = Abs ("state", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    1.19 +    fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    1.20        | quote_tr ts = raise TERM ("quote_tr", ts);
    1.21    in [("_quote", quote_tr)] end
    1.22  *};
    1.23  
    1.24  text {* basic examples *};
    1.25 -term "{. a + b + c .}";
    1.26 -term "{. a + b + c + `x + `y + 1 .}";
    1.27 -term "{. `(f w) + `x .}";
    1.28 -term "{. f (`x) (`y) z .}";
    1.29 +term ".(a + b + c).";
    1.30 +term ".(a + b + c + `x + `y + 1).";
    1.31 +term ".(`(f w) + `x).";
    1.32 +term ".(f `x `y z).";
    1.33  
    1.34  text {* advanced examples *};
    1.35 -term "{. {. `(`x) + `y .} .}";
    1.36 -term "{. {. `(`x) + `y .} o `f .}";
    1.37 -term "{. `(f o `g) .}";
    1.38 -term "{. {. `(`(f o `g)) .} .}";
    1.39 +term ".(.(` `x + `y).).";
    1.40 +term ".(.(` `x + `y). o `f).";
    1.41 +term ".(`(f o `g)).";
    1.42 +term ".(.(`(`(f o `g))).).";
    1.43  
    1.44  end;