# HG changeset patch
# User wenzelm
# Date 1395351267 -3600
# Node ID 797060c19f5c862e7b5dc505b08ae690d01ee527
# Parent  31e283f606e28e82801716a93ac64e858e020f0b
more symbols;

diff -r 31e283f606e2 -r 797060c19f5c src/HOL/ex/Antiquote.thy
--- 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
diff -r 31e283f606e2 -r 797060c19f5c src/HOL/ex/Multiquote.thy
--- 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