--- a/src/HOLCF/Discrete.thy Mon Jan 14 18:25:20 2008 +0100
+++ b/src/HOLCF/Discrete.thy Mon Jan 14 19:25:21 2008 +0100
@@ -15,15 +15,14 @@
subsection {* Type @{typ "'a discr"} is a partial order *}
-instance discr :: (type) sq_ord ..
-
-defs (overloaded)
-less_discr_def: "((op <<)::('a::type)discr=>'a discr=>bool) == op ="
+instantiation discr :: (type) po
+begin
-lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
-by (unfold less_discr_def) (rule refl)
+definition
+ less_discr_def [simp]:
+ "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
-instance discr :: (type) po
+instance
proof
fix x y z :: "'a discr"
show "x << x" by simp
@@ -31,6 +30,11 @@
{ assume "x << y" and "y << z" thus "x << z" by simp }
qed
+end
+
+lemma discr_less_eq [iff]: "((x::('a::type)discr) << y) = (x = y)"
+by simp
+
subsection {* Type @{typ "'a discr"} is a cpo *}
lemma discr_chain0: