# HG changeset patch
# User huffman
# Date 1200335121 -3600
# Node ID c00823ce7288116ab67dbfc0bf17a73edf01ecc2
# Parent  bb178c8251e0943c4e427b11ae10d53ec08d0e31
new-style class instantiation

diff -r bb178c8251e0 -r c00823ce7288 src/HOLCF/Discrete.thy
--- 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: