# HG changeset patch
# User paulson
# Date 943980814 -3600
# Node ID ecdedff41e67169758090d820b103b73e265de7b
# Parent  e3237d8c18d682eca4fb89f1296b7e755bb03a4a
deleted rogue copy of localTo_imp_o_localTo

diff -r e3237d8c18d6 -r ecdedff41e67 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Tue Nov 30 16:54:10 1999 +0100
+++ b/src/HOL/UNITY/Union.ML	Tue Nov 30 17:53:34 1999 +0100
@@ -371,12 +371,6 @@
 				  Join_left_absorb]) 1);
 qed "self_Join_LocalTo";
 
-Goalw [LOCALTO_def]
-     "[| G : v localTo[C] F;  F<=F' |] ==> G : v localTo[C] F'";
-by (Force_tac 1);
-qed "localTo_imp_o_localTo";
-
-
 
 (*** Higher-level rules involving localTo and Join ***)