# HG changeset patch
# User nipkow
# Date 908551926 -7200
# Node ID 8b872d546b9e5cf437bb546f99dbd48b9ddd2aa2
# Parent  204083e3f368d248cb625ccfa0a6363c926e1815
Installed trans_tac in solver of simpset().

diff -r 204083e3f368 -r 8b872d546b9e src/HOL/Arith.ML
--- 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);
diff -r 204083e3f368 -r 8b872d546b9e src/HOL/NatDef.ML
--- 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);