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