src/HOL/Nat.ML
changeset 1485 240cc98b94a7
parent 1475 7f5a4cd08209
child 1531 e5eb247ad13c
     1.1 --- a/src/HOL/Nat.ML	Fri Feb 09 12:18:02 1996 +0100
     1.2 +++ b/src/HOL/Nat.ML	Fri Feb 09 13:41:18 1996 +0100
     1.3 @@ -343,7 +343,7 @@
     1.4  by(nat_ind_tac "k" 1);
     1.5  by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
     1.6  by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
     1.7 -bind_thm("less_trans_Suc",result() RS mp);
     1.8 +qed_spec_mp "less_trans_Suc";
     1.9  
    1.10  (*"Less than" is a linear ordering*)
    1.11  goal Nat.thy "m<n | m=n | n<(m::nat)";