diff -r bb2dd95c8c5e -r a000b267be57 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Dec 02 11:44:55 2004 +0100
+++ b/src/HOL/HOL.thy	Thu Dec 02 11:59:34 2004 +0100
@@ -1160,7 +1160,15 @@
 
   | all_tr' [Const ("_bound",_) $ Free (v,_), 
                Const("op -->",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
-  (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
+  (if v=v' then Syntax.const "_leAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
+
+  | all_tr' [Const ("_bound",_) $ Free (v,_), 
+               Const("op -->",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  (if v=v' then Syntax.const "_gtAll" $ Syntax.mark_bound v' $ n $ P else raise Match)
+
+  | all_tr' [Const ("_bound",_) $ Free (v,_), 
+               Const("op -->",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  (if v=v' then Syntax.const "_geAll" $ Syntax.mark_bound v' $ n $ P else raise Match);
 
   fun ex_tr' [Const ("_bound",_) $ Free (v,_), 
                Const("op &",_) $ (Const ("op <",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
@@ -1168,7 +1176,16 @@
 
   | ex_tr' [Const ("_bound",_) $ Free (v,_), 
                Const("op &",_) $ (Const ("op <=",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] = 
-  (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
+  (if v=v' then Syntax.const "_leEx" $ Syntax.mark_bound v' $ n $ P else
+               raise Match)
+
+  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
+               Const("op &",_) $ (Const ("op <",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  (if v=v' then Syntax.const "_gtEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
+
+  | ex_tr' [Const ("_bound",_) $ Free (v,_), 
+               Const("op &",_) $ (Const ("op <=",_) $ n $ (Const ("_bound",_) $ Free (v',_))) $ P] = 
+  (if v=v' then Syntax.const "_geEx" $ Syntax.mark_bound v' $ n $ P else raise Match)
 in
 [("ALL ", all_tr'), ("EX ", ex_tr')]
 end