equal
deleted
inserted
replaced
277 done |
277 done |
278 |
278 |
279 |
279 |
280 subsection \<open>HOLCF type definition package\<close> |
280 subsection \<open>HOLCF type definition package\<close> |
281 |
281 |
282 ML_file "Tools/cpodef.ML" |
282 ML_file \<open>Tools/cpodef.ML\<close> |
283 |
283 |
284 end |
284 end |