equal
deleted
inserted
replaced
893 (* context setup *) |
893 (* context setup *) |
894 |
894 |
895 val setup = |
895 val setup = |
896 init_arith_data #> |
896 init_arith_data #> |
897 Simplifier.map_ss (fn ss => ss |
897 Simplifier.map_ss (fn ss => ss |
898 addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); |
898 addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); |
899 |
899 |
900 val global_setup = |
900 val global_setup = |
901 Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split)) |
901 Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split)) |
902 "declaration of split rules for arithmetic procedure" #> |
902 "declaration of split rules for arithmetic procedure" #> |
903 Method.setup @{binding linarith} |
903 Method.setup @{binding linarith} |