--- a/src/HOL/UNITY/Extend.ML Tue Apr 20 14:34:47 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML Tue Apr 20 14:35:12 1999 +0200
@@ -315,6 +315,13 @@
by (full_simp_tac (simpset() addsimps [slice_extend_set]) 1);
qed "extend_leadsto_eq";
+Goal "(extend h F : LeadsTo (extend_set h A) (extend_set h B)) = \
+\ (F : LeadsTo A B)";
+by (simp_tac
+ (simpset() addsimps [LeadsTo_def, reachable_extend_eq,
+ extend_leadsto_eq, extend_set_Int_distrib RS sym]) 1);
+qed "extend_LeadsTo";
+
(*** guarantees properties ***)