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