Simplifid proofs.
authornipkow
Sun Oct 27 13:47:02 1996 +0100 (1996-10-27)
changeset 213053b6e0bc8ccf
parent 2129 2ffe6e24f38d
child 2131 3106a99d30a5
Simplifid proofs.
src/HOL/IOA/NTP/Lemmas.ML
src/HOL/Lex/Prefix.ML
     1.1 --- a/src/HOL/IOA/NTP/Lemmas.ML	Fri Oct 25 15:02:09 1996 +0200
     1.2 +++ b/src/HOL/IOA/NTP/Lemmas.ML	Sun Oct 27 13:47:02 1996 +0100
     1.3 @@ -75,7 +75,6 @@
     1.4    by (nat_ind_tac "x" 1);
     1.5    by (Simp_tac 1);
     1.6    by (Asm_simp_tac 1);
     1.7 -  by (Fast_tac 1);
     1.8  qed "nonzero_is_succ";
     1.9  
    1.10  goal Arith.thy "(m::nat) < n --> m + p < n + p";
     2.1 --- a/src/HOL/Lex/Prefix.ML	Fri Oct 25 15:02:09 1996 +0200
     2.2 +++ b/src/HOL/Lex/Prefix.ML	Sun Oct 27 13:47:02 1996 +0100
     2.3 @@ -21,7 +21,6 @@
     2.4  goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
     2.5  by (list.induct_tac "xs" 1);
     2.6  by (Simp_tac 1);
     2.7 -by (Fast_tac 1);
     2.8  by (Simp_tac 1);
     2.9  qed "prefix_Nil";
    2.10  Addsimps [prefix_Nil];
    2.11 @@ -31,7 +30,6 @@
    2.12     "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
    2.13  by (list.induct_tac "xs" 1);
    2.14  by (Simp_tac 1);
    2.15 -by (Fast_tac 1);
    2.16  by (Simp_tac 1);
    2.17  by (Fast_tac 1);
    2.18  qed "prefix_Cons";