changeset 69605 | a96320074298 |
parent 67091 | 1393c2340eec |
child 69913 | ca515cf61651 |
--- a/src/HOL/Library/Old_Recdef.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Library/Old_Recdef.thy Sun Jan 06 15:04:34 2019 +0100 @@ -57,7 +57,7 @@ lemma tfl_exE: "\<exists>x. P x \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q \<Longrightarrow> Q" by blast -ML_file "old_recdef.ML" +ML_file \<open>old_recdef.ML\<close> subsection \<open>Rule setup\<close>