| changeset 69605 | a96320074298 |
| parent 69567 | 6b4c41037649 |
| child 77811 | ae9e6218443d |
--- a/src/HOL/Library/Case_Converter.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Library/Case_Converter.thy Sun Jan 06 15:04:34 2019 +0100 @@ -18,6 +18,6 @@ "missing_pattern_match = Code.abort" unfolding missing_pattern_match_def Code.abort_def .. -ML_file "case_converter.ML" +ML_file \<open>case_converter.ML\<close> end