src/HOL/arith_data.ML
changeset 5983 79e301a6a51b
parent 5771 7c2c8cf20221
     1.1 --- a/src/HOL/arith_data.ML	Fri Nov 27 16:54:59 1998 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Fri Nov 27 17:00:30 1998 +0100
     1.3 @@ -250,3 +250,8 @@
     1.4  Goal "m-n = 0  -->  n-m = 0  -->  m=n";
     1.5  by(simp_tac (simpset() addsplits [nat_diff_split]) 1);
     1.6  qed_spec_mp "diffs0_imp_equal";
     1.7 +
     1.8 +use"fast_nat_decider";
     1.9 +
    1.10 +simpset_ref () := (simpset() addSolver
    1.11 +  (fn thms => cut_facts_tac thms THEN' Fast_Nat_Decider.nat_arith_tac));