Installed trans_tac in solver of simpset().

--- a/src/HOL/Arith.ML	Fri Oct 16 12:23:07 1998 +0200
+++ b/src/HOL/Arith.ML	Fri Oct 16 17:32:06 1998 +0200
@@ -154,8 +154,6 @@
 Goal "n <= ((m + n)::nat)";
 by (induct_tac "m" 1);
 by (ALLGOALS Simp_tac);
-by (etac le_trans 1);
-by (rtac (lessI RS less_imp_le) 1);
 qed "le_add2";
 
 Goal "n <= ((n + m)::nat)";
@@ -183,12 +181,10 @@
 (*"i < j ==> i < m+j"*)
 bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
 
-Goal "i+j < (k::nat) ==> i<k";
-by (etac rev_mp 1);
+Goal "i+j < (k::nat) --> i<k";
 by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
-by (blast_tac (claset() addDs [Suc_lessD]) 1);
-qed "add_lessD1";
+qed_spec_mp "add_lessD1";
 
 Goal "~ (i+j < (i::nat))";
 by (rtac notI 1);

--- a/src/HOL/NatDef.ML	Fri Oct 16 12:23:07 1998 +0200
+++ b/src/HOL/NatDef.ML	Fri Oct 16 17:32:06 1998 +0200
@@ -615,5 +615,7 @@
 
 open Trans_Tac;
 
+simpset_ref () := (simpset() addSolver cut_trans_tac);
+
 (*** eliminates ~= in premises, which trans_tac cannot deal with ***)
 bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE);