New Asm_full_simp_tac shortens proof.

--- 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));