equal
deleted
inserted
replaced
805 addcongs [@{thm if_weak_cong}], |
805 addcongs [@{thm if_weak_cong}], |
806 number_of = number_of}) #> |
806 number_of = number_of}) #> |
807 add_discrete_type @{type_name nat}; |
807 add_discrete_type @{type_name nat}; |
808 |
808 |
809 fun add_arith_facts ss = |
809 fun add_arith_facts ss = |
810 add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss; |
810 Simplifier.add_prems (Arith_Data.get_arith_facts (Simplifier.the_context ss)) ss; |
811 |
811 |
812 val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc; |
812 val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc; |
813 |
813 |
814 |
814 |
815 (* generic refutation procedure *) |
815 (* generic refutation procedure *) |