| changeset 69605 | a96320074298 |
| parent 69593 | 3dda49e08b9d |
| child 70332 | 315489d836d8 |
--- a/src/HOL/Semiring_Normalization.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Semiring_Normalization.thy Sun Jan 06 15:04:34 2019 +0100 @@ -67,7 +67,7 @@ text \<open>Semiring normalization proper\<close> -ML_file "Tools/semiring_normalizer.ML" +ML_file \<open>Tools/semiring_normalizer.ML\<close> context comm_semiring_1 begin