author | nipkow |
Mon, 09 Feb 2009 22:14:33 +0100 | |
changeset 29850 | 14d9891c917b |
parent 29849 | a2baf1b221be |
child 29851 | 55ddff2ed906 |
--- a/src/HOL/Tools/lin_arith.ML Mon Feb 09 18:50:10 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Feb 09 22:14:33 2009 +0100 @@ -926,7 +926,8 @@ val setup = init_arith_data #> Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc] - addSolver (mk_solver' "lin_arith" Fast_Arith.cut_lin_arith_tac)) #> + addSolver (mk_solver' "lin_arith" + (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #> Context.mapping (setup_options #> Method.add_methods