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