--- 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)"})
*}