--- a/src/HOLCF/Porder.ML Wed Apr 23 13:23:05 1997 +0200
+++ b/src/HOLCF/Porder.ML Thu Apr 24 09:34:59 1997 +0200
@@ -9,30 +9,6 @@
open Porder;
(* ------------------------------------------------------------------------ *)
-(* the reverse law of anti--symmetrie of << *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac conjI 1),
- ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
- ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
- ]);
-
-
-qed_goal "box_less" thy
-"[| a << b; c << a; b << d|] ==> c << d"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac trans_less 1),
- (etac trans_less 1),
- (atac 1)
- ]);
-
-(* ------------------------------------------------------------------------ *)
(* lubs are unique *)
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Porder0.ML Wed Apr 23 13:23:05 1997 +0200
+++ b/src/HOLCF/Porder0.ML Thu Apr 24 09:34:59 1997 +0200
@@ -40,3 +40,28 @@
(atac 1),
(etac spec 1)
])));
+
+(* ------------------------------------------------------------------------ *)
+(* the reverse law of anti--symmetrie of << *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "antisym_less_inverse" thy "x=y ==> x << y & y << x"
+(fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (rtac conjI 1),
+ ((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
+ ((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
+ ]);
+
+
+qed_goal "box_less" thy
+"[| a << b; c << a; b << d|] ==> c << d"
+ (fn prems =>
+ [
+ (cut_facts_tac prems 1),
+ (etac trans_less 1),
+ (etac trans_less 1),
+ (atac 1)
+ ]);
+