--- a/QuotTest.thy	Sat Oct 24 16:15:33 2009 +0200
+++ b/QuotTest.thy	Sat Oct 24 16:31:07 2009 +0200
@@ -9,7 +9,7 @@
 | lam  "nat" "trm"
 
 axiomatization
-  RR :: "trm ⇒ trm ⇒ bool"
+  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
 where
   r_eq: "EQUIV RR"
 
@@ -44,7 +44,7 @@
 | app'  "'a trm'" "'a trm'"
 | lam'  "'a" "'a trm'"
 
-consts R' :: "'a trm' ⇒ 'a trm' ⇒ bool"
+consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
 quotient qtrm' = "'a trm'" / "R'"
@@ -66,7 +66,7 @@
 | ap "t list"
 | lm "string" "t"
 
-consts Rt :: "t ⇒ t ⇒ bool"
+consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
 axioms t_eq: "EQUIV Rt"
 
 quotient qt = "t" / "Rt"
@@ -74,7 +74,7 @@
 
 
 ML {*
-  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt ⇒ qt) ⇒ qt) ⇒ qt) list) * nat"}
+  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
@@ -88,7 +88,7 @@
 *}
 
 ML {*
-  get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt ⇒ qt) ⇒ qt"}
+  get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
   |> fst
   |> Syntax.pretty_term @{context}
   |> Pretty.string_of
@@ -96,7 +96,7 @@
 *}
 
 (* A test whether get_fun works properly
-consts bla :: "(t ⇒ t) ⇒ t"
+consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
 local_setup {*
   fn lthy => (Toplevel.program (fn () =>
     make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
@@ -122,9 +122,9 @@
 datatype 'a t' =
   vr' "string"
 | ap' "('a t') * ('a t')"
-| lm' "'a" "string ⇒ ('a t')"
+| lm' "'a" "string \<Rightarrow> ('a t')"
 
-consts Rt' :: "('a t') ⇒ ('a t') ⇒ bool"
+consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 axioms t_eq': "EQUIV Rt'"
 
 quotient qt' = "'a t'" / "Rt'"
@@ -149,41 +149,41 @@
 
 text {* Tests of regularise *}
 ML {*
-  cterm_of @{theory} (regularise @{term "λx :: int. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "λx :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "∀x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "∃x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "All (P :: trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
 *}
 
 ML {*
-  cterm_of @{theory} (regularise @{term "∃(y::trm). P (λ(x::trm). y)"} @{typ "trm"}
+  cterm_of @{theory} (regularise @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"} @{typ "trm"}
      @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "∃(y::trm). P (λ(x::trm). y)"})
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>(y::trm). P (\<lambda>(x::trm). y)"})
 *}
 
 ML {*
-  cterm_of @{theory} (regularise @{term "λx::trm. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "λx::trm. x"})
+  cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
 *}
 
 ML {*
-  cterm_of @{theory} (regularise @{term "∀(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "∀(x::trm) (y::trm). P x y"})
+  cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
 *}
 
 ML {*
-  cterm_of @{theory} (regularise @{term "∀x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "∀x::trm. P x"})
+  cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
 *}
 
 ML {*
-  cterm_of @{theory} (regularise @{term "∃x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "∃x::trm. P x"})
+  cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
 *}
 
 (* my version is not eta-expanded, but that should be OK *)
 ML {*
-  cterm_of @{theory} (regularise @{term "All (P::trm ⇒ bool)"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm ⇒ bool)"})
+  cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
 *}