# HG changeset patch
# User nipkow
# Date 846420422 -3600
# Node ID 53b6e0bc8ccfdce5b36ab74d4addd48541427d10
# Parent  2ffe6e24f38d53df72695a7b80ff1d3941421d98
Simplifid proofs.

diff -r 2ffe6e24f38d -r 53b6e0bc8ccf src/HOL/IOA/NTP/Lemmas.ML
--- a/src/HOL/IOA/NTP/Lemmas.ML	Fri Oct 25 15:02:09 1996 +0200
+++ b/src/HOL/IOA/NTP/Lemmas.ML	Sun Oct 27 13:47:02 1996 +0100
@@ -75,7 +75,6 @@
   by (nat_ind_tac "x" 1);
   by (Simp_tac 1);
   by (Asm_simp_tac 1);
-  by (Fast_tac 1);
 qed "nonzero_is_succ";
 
 goal Arith.thy "(m::nat) < n --> m + p < n + p";
diff -r 2ffe6e24f38d -r 53b6e0bc8ccf src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Fri Oct 25 15:02:09 1996 +0200
+++ b/src/HOL/Lex/Prefix.ML	Sun Oct 27 13:47:02 1996 +0100
@@ -21,7 +21,6 @@
 goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (Fast_tac 1);
 by (Simp_tac 1);
 qed "prefix_Nil";
 Addsimps [prefix_Nil];
@@ -31,7 +30,6 @@
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
 by (list.induct_tac "xs" 1);
 by (Simp_tac 1);
-by (Fast_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed "prefix_Cons";