--- a/src/HOLCF/IOA/NTP/Impl.ML Wed Mar 11 09:50:31 1998 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.ML Wed Mar 11 10:17:16 1998 +0100
@@ -278,14 +278,6 @@
by (rtac impI 1);
by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
by (Asm_full_simp_tac 1);
- by (REPEAT (etac conjE 1));
- by (dtac mp 1);
- by (assume_tac 1);
- by (etac allE 1);
- by (dtac (imp_or_lem RS iffD1) 1);
- by (dtac mp 1);
- by (assume_tac 1);
- by (assume_tac 1);
qed "inv3";
@@ -308,7 +300,7 @@
(* 10 - 2 *)
by (EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]);
-
+
(* 2 b *)
by (strip_tac 1 THEN REPEAT (etac conjE 1));