# HG changeset patch
# User huffman
# Date 1181163989 -7200
# Node ID 07ae93e58fead3e1ad917f3ca25e257071603b4b
# Parent  c7ab7051aba0110848f902975e2302732cd00054
use new-style class for sq_ord; rename op << to sq_le

diff -r c7ab7051aba0 -r 07ae93e58fea src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Jun 06 21:24:35 2007 +0200
+++ b/src/HOLCF/Porder.thy	Wed Jun 06 23:06:29 2007 +0200
@@ -11,19 +11,17 @@
 
 subsection {* Type class for partial orders *}
 
-	-- {* introduce a (syntactic) class for the constant @{text "<<"} *}
-axclass sq_ord < type
+class sq_ord = type +
+  fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
-	-- {* characteristic constant @{text "<<"} for po *}
-consts
-  "<<"          :: "['a,'a::sq_ord] => bool"        (infixl "<<" 55)
+notation
+  sq_le (infixl "<<" 55)
 
-syntax (xsymbols)
-  "<<"       :: "['a,'a::sq_ord] => bool"        (infixl "\<sqsubseteq>" 55)
+notation (xsymbols)
+  sq_le (infixl "\<sqsubseteq>" 55)
 
 axclass po < sq_ord
-        -- {* class axioms: *}
-  refl_less [iff]: "x \<sqsubseteq> x"        
+  refl_less [iff]: "x \<sqsubseteq> x"
   antisym_less:    "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"    
   trans_less:      "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
 
diff -r c7ab7051aba0 -r 07ae93e58fea src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Wed Jun 06 21:24:35 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Wed Jun 06 23:06:29 2007 +0200
@@ -99,7 +99,7 @@
 
 (* ----- qualified names of HOLCF constants ----- *)
 
-val lessN      = "Porder.<<"
+val lessN      = @{const_name Porder.sq_le};
 val UU_N       = "Pcpo.UU";
 val admN       = "Adm.adm";
 val compactN   = "Adm.compact";
diff -r c7ab7051aba0 -r 07ae93e58fea src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Wed Jun 06 21:24:35 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Wed Jun 06 23:06:29 2007 +0200
@@ -87,7 +87,7 @@
 
     val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
     val RepC = Const (full Rep_name, newT --> oldT);
-    fun lessC T = Const ("Porder.<<", T --> T --> HOLogic.boolT);
+    fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT);
     val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT,
       Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))));