src/HOL/Set.thy

--- a/src/HOL/Set.thy	Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Set.thy	Fri Mar 17 09:34:23 2006 +0100
@@ -168,7 +168,7 @@
     fun less_tr' _ (Type ("fun", (Type ("set", _) :: _))) ts =
           list_comb (Syntax.const "_setless", ts)
       | less_tr' _ _ _ = raise Match;
-  in [("op <=", le_tr'), ("op <", less_tr')] end
+  in [("Orderings.less_eq", le_tr'), ("Orderings.less", less_tr')] end
 *}
 
 
@@ -208,26 +208,26 @@
 let
   fun
     all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-             Const("op -->",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+             Const("op -->",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setlessAll" $ Syntax.mark_bound v' $ n $ P
    else raise Match)
 
   | all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-             Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+             Const("op -->",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setleAll" $ Syntax.mark_bound v' $ n $ P
    else raise Match);
 
   fun
     ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-            Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+            Const("op &",_) $ (Const ("Orderings.less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setlessEx" $ Syntax.mark_bound v' $ n $ P
    else raise Match)
 
   | ex_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
-            Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
+            Const("op &",_) $ (Const ("Orderings.less_eq",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
   (if v=v' andalso T="set"
    then Syntax.const "_setleEx" $ Syntax.mark_bound v' $ n $ P
    else raise Match)