src/HOL/ex/Multiquote.thy
changeset 10838 9423817dee84
parent 10834 a7897aebbffc
child 11020 646c929b6293
     1.1 --- a/src/HOL/ex/Multiquote.thy	Wed Jan 10 00:14:52 2001 +0100
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Wed Jan 10 00:15:33 2001 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  syntax
     1.6    "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
     1.7 -  "_antiquote" :: "('a => 'b) => 'b"         ("_" [1000] 1000)
     1.8 +  "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
     1.9  
    1.10  parse_translation {*
    1.11    let
    1.12 @@ -35,14 +35,14 @@
    1.13  
    1.14  text {* basic examples *}
    1.15  term ".(a + b + c)."
    1.16 -term ".(a + b + c + x + y + 1)."
    1.17 -term ".((f w) + x)."
    1.18 -term ".(f x y z)."
    1.19 +term ".(a + b + c + \<acute>x + \<acute>y + 1)."
    1.20 +term ".(\<acute>(f w) + \<acute>x)."
    1.21 +term ".(f \<acute>x \<acute>y z)."
    1.22  
    1.23  text {* advanced examples *}
    1.24 -term ".(.( x + y).)."
    1.25 -term ".(.( x + y). o f)."
    1.26 -term ".((f o g))."
    1.27 -term ".(.(  (f o g) ).)."
    1.28 +term ".(.(\<acute>\<acute>x + \<acute>y).)."
    1.29 +term ".(.(\<acute>\<acute>x + \<acute>y). o \<acute>f)."
    1.30 +term ".(\<acute>(f o \<acute>g))."
    1.31 +term ".(.( \<acute>\<acute>(f o \<acute>g) ).)."
    1.32  
    1.33  end