equal
deleted
inserted
replaced
924 (* context setup *) |
924 (* context setup *) |
925 |
925 |
926 val setup = |
926 val setup = |
927 init_arith_data #> |
927 init_arith_data #> |
928 Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc] |
928 Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc] |
929 addSolver (mk_solver' "lin_arith" Fast_Arith.cut_lin_arith_tac)) #> |
929 addSolver (mk_solver' "lin_arith" |
|
930 (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #> |
930 Context.mapping |
931 Context.mapping |
931 (setup_options #> |
932 (setup_options #> |
932 Method.add_methods |
933 Method.add_methods |
933 [("arith", arith_method, "decide linear arithmetic")] #> |
934 [("arith", arith_method, "decide linear arithmetic")] #> |
934 Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add, |
935 Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add, |