Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removal of Always_StableI
authorpaulson
Thu, 27 May 1999 11:22:10 +0200
changeset 6740 5b5bf511fdd5
parent 6739 66e4118eead9
child 6741 540fc00ec32b
removal of Always_StableI
src/HOL/UNITY/Lift.ML file | annotate | diff | comparison | revisions
src/HOL/UNITY/NSP_Bad.ML file | annotate | diff | comparison | revisions 
--- 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);
--- 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];
isabelle