changeset 2056 | 93c093620c28 |
parent 1985 | 84cf16192e03 |
child 4089 | 96fba19bcbe2 |
--- a/src/HOL/Lex/Auto.ML Mon Oct 07 10:26:00 1996 +0200 +++ b/src/HOL/Lex/Auto.ML Mon Oct 07 10:28:44 1996 +0200 @@ -34,6 +34,5 @@ by(asm_simp_tac (!simpset addsimps [eq_sym_conv]) 1); by(res_inst_tac [("x","x#us")] exI 1); by(Asm_simp_tac 1); -by (Fast_tac 1); qed"acc_prefix_Cons"; Addsimps [acc_prefix_Cons];