--- a/src/HOL/UNITY/SubstAx.ML Fri Sep 11 16:25:24 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Fri Sep 11 16:25:40 1998 +0200
@@ -100,7 +100,6 @@
Goal "[| LeadsTo prg A A'; id: Acts prg; \
\ B <= A; A' <= B' |] \
\ ==> LeadsTo prg B B'";
-(*PROOF FAILED unless the Trans rule is last*)
by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
@@ -177,11 +176,7 @@
This is the most useful form of the "disjunction" rule*)
Goal "[| LeadsTo prg (A-B) C; LeadsTo prg (A Int B) C; id: Acts prg |] \
\ ==> LeadsTo prg A C";
-by (stac (Un_Diff_Int RS sym) 1 THEN rtac LeadsTo_Un 1);
-by (REPEAT (assume_tac 1));
-(*One step, but PROOF FAILED...
- by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
-*)
+by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
qed "LeadsTo_Diff";