src/HOL/W0/W.ML
changeset 4033 43ec35b5054d
parent 3919 c036caebfc75
child 4089 96fba19bcbe2
--- a/src/HOL/W0/W.ML	Thu Oct 30 09:45:03 1997 +0100
+++ b/src/HOL/W0/W.ML	Thu Oct 30 09:46:11 1997 +0100
@@ -65,7 +65,6 @@
 by (eres_inst_tac [("x","sa")] allE 1);
 by (eres_inst_tac [("x","ta")] allE 1);
 by (eres_inst_tac [("x","nb")] allE 1);
-by (etac conjE 1);
 by (res_inst_tac [("j","na")] le_trans 1); 
 by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);