# HG changeset patch
# User paulson
# Date 927796930 -7200
# Node ID 5b5bf511fdd5fc7b6c3d6cadde7da3aeb01fd18a
# Parent  66e4118eead972ddf8fbb0c64fec9fd7f5fae732
removal of Always_StableI

diff -r 66e4118eead9 -r 5b5bf511fdd5 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Thu May 27 11:19:45 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML	Thu May 27 11:22:10 1999 +0200
@@ -101,7 +101,8 @@
 
 Goal "Lift : Always bounded";
 by (rtac AlwaysI 1);
-by (rtac (Always_Int_rule [moving_up, moving_down] RS Always_StableI) 2);
+by (rtac (Always_Int_rule [moving_up, moving_down] RS 
+	  Always_ConstrainsI RS StableI) 2);
 by (Force_tac 1);
 by (constrains_tac 1);
 by (ALLGOALS Clarify_tac);
diff -r 66e4118eead9 -r 5b5bf511fdd5 src/HOL/UNITY/NSP_Bad.ML
--- a/src/HOL/UNITY/NSP_Bad.ML	Thu May 27 11:19:45 1999 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Thu May 27 11:22:10 1999 +0200
@@ -75,7 +75,7 @@
      [rtac AlwaysI 1,
       Force_tac 1,
       (*"reachable" gets in here*)
-      rtac (Always_reachable RS Always_StableI) 1,
+      rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
       ns_constrains_tac 1];