# HG changeset patch
# User nipkow
# Date 889607836 -3600
# Node ID 0196377b57036b0625230e8b8217fc390e6f1a42
# Parent  b1d916e8a853cbfddd0bb64387195b590be1afb5
New Asm_full_simp_tac shortens proof.

diff -r b1d916e8a853 -r 0196377b5703 src/HOLCF/IOA/NTP/Impl.ML
--- 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));