# HG changeset patch
# User slotosch
# Date 861867299 -7200
# Node ID 7a5611f66b7286349d671f1fafec55ef996e18b3
# Parent  ab6bcbd130a141fd8086b9ac8d3e1e85aeaa4dd8
moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML

diff -r ab6bcbd130a1 -r 7a5611f66b72 src/HOLCF/Porder.ML
--- 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                                                          *)
 (* ------------------------------------------------------------------------ *)
 
diff -r ab6bcbd130a1 -r 7a5611f66b72 src/HOLCF/Porder0.ML
--- 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)
+        ]);
+