# HG changeset patch
# User paulson
# Date 961666488 -7200
# Node ID 89ca2a172f84b496eada182f5635a9a402085023
# Parent  ef56f093259d8bb62cfe045b9ed3fc43e7adedb4
new thoerem Always_Follows2; renamed Always_Follows -> Always_Follows1

diff -r ef56f093259d -r 89ca2a172f84 src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Wed Jun 21 20:38:25 2000 +0200
+++ b/src/HOL/UNITY/Follows.ML	Thu Jun 22 11:34:48 2000 +0200
@@ -98,7 +98,19 @@
 by (dtac Always_Int_I 1);
 by (assume_tac 1);
 by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
-qed "Always_Follows";
+qed "Always_Follows1";
+
+Goalw [Follows_def, Increasing_def, Stable_def]
+     "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'"; 
+by Auto_tac;
+by (etac Always_LeadsTo_weaken 3);
+by (eres_inst_tac [("A", "{s. z <= g s}"), ("A'", "{s. z <= g s}")] 
+                  Always_Constrains_weaken 1);
+by Auto_tac;
+by (dtac Always_Int_I 1);
+by (assume_tac 1);
+by (force_tac (claset() addIs [Always_weaken], simpset()) 1);
+qed "Always_Follows2";
 
 
 (** Union properties (with the subset ordering) **)