typo
authorhaftmann
Sat Jan 10 10:40:11 2015 +0100 (2015-01-10)
changeset 59335e743ce816cf6
parent 59334 f0141b991c8f
child 59336 a95b6f608a73
child 59337 6adaa4a17cfb
typo
src/Doc/Codegen/Evaluation.thy
     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"},