eliminated suspicious Unicode;
authorwenzelm
Wed Jun 06 11:41:54 2018 +0200 (11 months ago)
changeset 68390c558a2202f32
parent 68389 1c84a8c513af
child 68391 9b4f60bdad54
eliminated suspicious Unicode;
src/HOL/Library/Code_Lazy.thy
     1.1 --- a/src/HOL/Library/Code_Lazy.thy	Wed Jun 06 11:41:37 2018 +0200
     1.2 +++ b/src/HOL/Library/Code_Lazy.thy	Wed Jun 06 11:41:54 2018 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  text \<open>
     1.5    This theory and the CodeLazy tool described in @{cite "LochbihlerStoop2018"}.
     1.6  
     1.7 -  It hooks into Isabelle’s code generator such that the generated code evaluates a user-specified
     1.8 +  It hooks into Isabelle's code generator such that the generated code evaluates a user-specified
     1.9    set of type constructors lazily, even in target languages with eager evaluation.
    1.10    The lazy type must be algebraic, i.e., values must be built from constructors and a
    1.11    corresponding case operator decomposes them. Every datatype and codatatype is algebraic