# HG changeset patch
# User paulson
# Date 941119632 -7200
# Node ID 6b3e345c47b359ebcffe2e4b424609049dc9dd2c
# Parent  e7beff82e1ba553ab520a3f56028f0e4f9e16930
localTo_imp_o_localTo is now really an implication

diff -r e7beff82e1ba -r 6b3e345c47b3 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Thu Oct 28 16:06:07 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Thu Oct 28 16:07:12 1999 +0200
@@ -111,11 +111,11 @@
 by (Force_tac 1);
 by (rtac Stable_Int 1);
 by (full_simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 2);
-by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
+by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo]
 	               addIs [Increasing_localTo_Stable, 
 			      stable_size_rel_le_giv]) 2);
 by (full_simp_tac (simpset() addsimps [Join_localTo]) 1);
-by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
+by (fast_tac (claset() addEs [rewrite_o localTo_imp_o_localTo]
 	               addIs [stable_localTo_stable2 RS stable_imp_Stable,
 			      stable_size_ask_le_rel]) 1);
 val lemma1 = result();
diff -r e7beff82e1ba -r 6b3e345c47b3 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Thu Oct 28 16:06:07 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Thu Oct 28 16:07:12 1999 +0200
@@ -334,9 +334,8 @@
 qed "localTo_imp_LocalTo";
 
 Goalw [LOCALTO_def, stable_def, constrains_def]
-     "v localTo[C] F <= (f o v) localTo[C] F";
-by (Clarify_tac 1);
-by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
+     "G : v localTo[C] F ==> G : (f o v) localTo[C] F";
+by (Force_tac 1);
 qed "localTo_imp_o_localTo";
 
 (*NOT USED*)