changeset 69605 | a96320074298 |
parent 69597 | ff784d5a5bfb |
child 69913 | ca515cf61651 |
--- a/src/HOL/HOLCF/Fixrec.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/HOLCF/Fixrec.thy Sun Jan 06 15:04:34 2019 +0100 @@ -224,8 +224,8 @@ subsection \<open>Initializing the fixrec package\<close> -ML_file "Tools/holcf_library.ML" -ML_file "Tools/fixrec.ML" +ML_file \<open>Tools/holcf_library.ML\<close> +ML_file \<open>Tools/fixrec.ML\<close> method_setup fixrec_simp = \<open> Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)