src/Doc/Codegen/Evaluation.thy
changeset 59335 e743ce816cf6
parent 59334 f0141b991c8f
child 59377 056945909f60
     1.1 --- a/src/Doc/Codegen/Evaluation.thy	Sat Jan 10 10:24:30 2015 +0100
     1.2 +++ b/src/Doc/Codegen/Evaluation.thy	Sat Jan 10 10:40:11 2015 +0100
     1.3 @@ -234,7 +234,7 @@
     1.4  text {*
     1.5    By virtue of @{fact interp.simps}, @{ML "Reification.conv"} provides a conversion
     1.6    which, for this concrete example, yields @{thm thm [no_vars]}.  Note that the argument
     1.7 -  to @{const interp} does not contain any free variables and can this be evaluated
     1.8 +  to @{const interp} does not contain any free variables and can thus be evaluated
     1.9    using evaluation.
    1.10  
    1.11    A less meager example can be found in the AFP, session @{text "Regular-Sets"},