Installed trans_tac in solver of simpset().
authornipkow
Fri Oct 16 17:32:06 1998 +0200 (1998-10-16)
changeset 56548b872d546b9e
parent 5653 204083e3f368
child 5655 afd75136b236
Installed trans_tac in solver of simpset().
src/HOL/Arith.ML
src/HOL/NatDef.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Oct 16 12:23:07 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Oct 16 17:32:06 1998 +0200
     1.3 @@ -154,8 +154,6 @@
     1.4  Goal "n <= ((m + n)::nat)";
     1.5  by (induct_tac "m" 1);
     1.6  by (ALLGOALS Simp_tac);
     1.7 -by (etac le_trans 1);
     1.8 -by (rtac (lessI RS less_imp_le) 1);
     1.9  qed "le_add2";
    1.10  
    1.11  Goal "n <= ((n + m)::nat)";
    1.12 @@ -183,12 +181,10 @@
    1.13  (*"i < j ==> i < m+j"*)
    1.14  bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
    1.15  
    1.16 -Goal "i+j < (k::nat) ==> i<k";
    1.17 -by (etac rev_mp 1);
    1.18 +Goal "i+j < (k::nat) --> i<k";
    1.19  by (induct_tac "j" 1);
    1.20  by (ALLGOALS Asm_simp_tac);
    1.21 -by (blast_tac (claset() addDs [Suc_lessD]) 1);
    1.22 -qed "add_lessD1";
    1.23 +qed_spec_mp "add_lessD1";
    1.24  
    1.25  Goal "~ (i+j < (i::nat))";
    1.26  by (rtac notI 1);
     2.1 --- a/src/HOL/NatDef.ML	Fri Oct 16 12:23:07 1998 +0200
     2.2 +++ b/src/HOL/NatDef.ML	Fri Oct 16 17:32:06 1998 +0200
     2.3 @@ -615,5 +615,7 @@
     2.4  
     2.5  open Trans_Tac;
     2.6  
     2.7 +simpset_ref () := (simpset() addSolver cut_trans_tac);
     2.8 +
     2.9  (*** eliminates ~= in premises, which trans_tac cannot deal with ***)
    2.10  bind_thm("nat_neqE", nat_neq_iff RS iffD1 RS disjE);