src/HOL/Library/Code_Lazy.thy
changeset 69690 1fb204399d8d
parent 69605 a96320074298
     1.1 --- a/src/HOL/Library/Code_Lazy.thy	Fri Jan 18 19:48:04 2019 -0500
     1.2 +++ b/src/HOL/Library/Code_Lazy.thy	Sat Jan 19 07:19:16 2019 +0000
     1.3 @@ -165,10 +165,12 @@
     1.4  
     1.5  
     1.6  code_printing
     1.7 -  code_module Lazy \<rightharpoonup> (Haskell) 
     1.8 -\<open>newtype Lazy a = Lazy a;
     1.9 -delay f = Lazy (f ());
    1.10 -force (Lazy x) = x;\<close> for type_constructor lazy constant delay force
    1.11 +  code_module Lazy \<rightharpoonup> (Haskell) \<open>
    1.12 +module Lazy(Lazy, delay, force) where
    1.13 +
    1.14 +newtype Lazy a = Lazy a
    1.15 +delay f = Lazy (f ())
    1.16 +force (Lazy x) = x\<close> for type_constructor lazy constant delay force
    1.17  | type_constructor lazy \<rightharpoonup> (Haskell) "Lazy.Lazy _"
    1.18  | constant delay \<rightharpoonup> (Haskell) "Lazy.delay"
    1.19  | constant force \<rightharpoonup> (Haskell) "Lazy.force"