# 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 \ 'a \ 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 "\" 55) +notation (xsymbols) + sq_le (infixl "\" 55) axclass po < sq_ord - -- {* class axioms: *} - refl_less [iff]: "x \ x" + refl_less [iff]: "x \ x" antisym_less: "\x \ y; y \ x\ \ x = y" trans_less: "\x \ y; y \ z\ \ x \ 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)))));