changeset 69605 | a96320074298 |
parent 69593 | 3dda49e08b9d |
child 72581 | de581f98a3a1 |
--- a/src/HOL/Quickcheck_Random.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Quickcheck_Random.thy Sun Jan 06 15:04:34 2019 +0100 @@ -209,8 +209,8 @@ subsection \<open>Deriving random generators for datatypes\<close> -ML_file "Tools/Quickcheck/quickcheck_common.ML" -ML_file "Tools/Quickcheck/random_generators.ML" +ML_file \<open>Tools/Quickcheck/quickcheck_common.ML\<close> +ML_file \<open>Tools/Quickcheck/random_generators.ML\<close> subsection \<open>Code setup\<close>