equal
deleted
inserted
replaced
205 |
205 |
206 subsection {* Deriving random generators for datatypes *} |
206 subsection {* Deriving random generators for datatypes *} |
207 |
207 |
208 ML_file "Tools/Quickcheck/quickcheck_common.ML" |
208 ML_file "Tools/Quickcheck/quickcheck_common.ML" |
209 ML_file "Tools/Quickcheck/random_generators.ML" |
209 ML_file "Tools/Quickcheck/random_generators.ML" |
210 setup Random_Generators.setup |
|
211 |
210 |
212 |
211 |
213 subsection {* Code setup *} |
212 subsection {* Code setup *} |
214 |
213 |
215 code_printing |
214 code_printing |