equal
deleted
inserted
replaced
1760 end |
1760 end |
1761 |
1761 |
1762 text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close> |
1762 text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close> |
1763 |
1763 |
1764 named_theorems arith "arith facts -- only ground formulas" |
1764 named_theorems arith "arith facts -- only ground formulas" |
1765 ML_file "Tools/arith_data.ML" |
1765 ML_file \<open>Tools/arith_data.ML\<close> |
1766 |
1766 |
1767 ML_file "~~/src/Provers/Arith/cancel_div_mod.ML" |
1767 ML_file \<open>~~/src/Provers/Arith/cancel_div_mod.ML\<close> |
1768 |
1768 |
1769 ML \<open> |
1769 ML \<open> |
1770 structure Cancel_Div_Mod_Ring = Cancel_Div_Mod |
1770 structure Cancel_Div_Mod_Ring = Cancel_Div_Mod |
1771 ( |
1771 ( |
1772 val div_name = \<^const_name>\<open>divide\<close>; |
1772 val div_name = \<^const_name>\<open>divide\<close>; |