changeset 69605 | a96320074298 |
parent 61383 | 6762c8445138 |
child 74607 | 7f6178b655a8 |
--- a/src/HOL/Library/Rewrite.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Library/Rewrite.thy Sun Jan 06 15:04:34 2019 +0100 @@ -30,7 +30,7 @@ apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+ done -ML_file "cconv.ML" -ML_file "rewrite.ML" +ML_file \<open>cconv.ML\<close> +ML_file \<open>rewrite.ML\<close> end