| changeset 69605 | a96320074298 |
| parent 69593 | 3dda49e08b9d |
| child 76213 | e44d86131648 |
--- a/src/ZF/ArithSimp.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/ZF/ArithSimp.thy Sun Jan 06 15:04:34 2019 +0100 @@ -9,9 +9,9 @@ imports Arith begin -ML_file "~~/src/Provers/Arith/cancel_numerals.ML" -ML_file "~~/src/Provers/Arith/combine_numerals.ML" -ML_file "arith_data.ML" +ML_file \<open>~~/src/Provers/Arith/cancel_numerals.ML\<close> +ML_file \<open>~~/src/Provers/Arith/combine_numerals.ML\<close> +ML_file \<open>arith_data.ML\<close> subsection\<open>Difference\<close>