| changeset 69272 | 15e9ed5b28fb |
| parent 69216 | 1a52baa70aed |
| child 69528 | 9d0e492e3229 |
--- a/src/HOL/Library/Code_Lazy.thy Thu Nov 08 22:02:07 2018 +0100 +++ b/src/HOL/Library/Code_Lazy.thy Thu Nov 08 22:29:09 2018 +0100 @@ -39,7 +39,7 @@ ML_file "case_converter.ML" -subsection \<open>The type @{text lazy}\<close> +subsection \<open>The type \<open>lazy\<close>\<close> typedef 'a lazy = "UNIV :: 'a set" .. setup_lifting type_definition_lazy