equal
deleted
inserted
replaced
899 (* context setup *) |
899 (* context setup *) |
900 |
900 |
901 val setup = |
901 val setup = |
902 init_arith_data #> |
902 init_arith_data #> |
903 Simplifier.map_ss (fn ss => ss |
903 Simplifier.map_ss (fn ss => ss |
904 addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); |
904 addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac))); |
905 |
905 |
906 val global_setup = |
906 val global_setup = |
907 Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split)) |
907 Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split)) |
908 "declaration of split rules for arithmetic procedure" #> |
908 "declaration of split rules for arithmetic procedure" #> |
909 Method.setup @{binding linarith} |
909 Method.setup @{binding linarith} |