# HG changeset patch
# User paulson
# Date 924611712 -7200
# Node ID 1c8f48966033071a2f47f3113094fc3cf51a2402
# Parent  c97d8058157220b7da280f7140de257f8640da5a
new result extend_LeadsTo

diff -r c97d80581572 -r 1c8f48966033 src/HOL/UNITY/Extend.ML
--- 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 ***)