src/HOL/Arith.ML
changeset 7570 a9391550eea1
parent 7548 9e29a3af64ab
child 7582 2650c9c2ab7f
     1.1 --- a/src/HOL/Arith.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/HOL/Arith.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -1000,7 +1000,8 @@
     1.4  fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
     1.5  solver all the time rather than add the additional check. *)
     1.6  
     1.7 -simpset_ref () := (simpset() addSolver Fast_Arith.cut_lin_arith_tac);
     1.8 +simpset_ref () := (simpset() addSolver
     1.9 +   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
    1.10  
    1.11  (* Elimination of `-' on nat due to John Harrison *)
    1.12  Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";