| changeset 8042 | ecdedff41e67 |
| parent 8041 | e3237d8c18d6 |
| child 8055 | bb15396278fb |
--- 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 ***)