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;
```