--- a/src/HOL/ex/Antiquote.thy Thu Mar 20 22:00:13 2014 +0100
+++ b/src/HOL/ex/Antiquote.thy Thu Mar 20 22:34:27 2014 +0100
@@ -13,14 +13,14 @@
syntax.
*}
-definition var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999)
+definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" ("VAR _" [1000] 999)
where "var x env = env x"
-definition Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
+definition Expr :: "(('a \<Rightarrow> nat) \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
where "Expr exp env = exp env"
syntax
- "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999)
+ "_Expr" :: "'a \<Rightarrow> 'a" ("EXPR _" [1000] 999)
parse_translation {*
[Syntax_Trans.quote_antiquote_tr
--- a/src/HOL/ex/Multiquote.thy Thu Mar 20 22:00:13 2014 +0100
+++ b/src/HOL/ex/Multiquote.thy Thu Mar 20 22:34:27 2014 +0100
@@ -14,8 +14,8 @@
*}
syntax
- "_quote" :: "'b => ('a => 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000)
- "_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000)
+ "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000)
+ "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
parse_translation {*
let
@@ -43,8 +43,8 @@
text {* advanced examples *}
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
-term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>"
-term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>"
-term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>"
+term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f \<circ> \<acute>g)\<guillemotright>\<guillemotright>"
end