src/Doc/Isar_Ref/Inner_Syntax.thy
changeset 60254 52110106c0ca
parent 59783 00b62aa9f430
child 60270 a147272b16f9
     1.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun May 03 23:41:24 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon May 04 19:55:30 2015 +0200
     1.3 @@ -1023,7 +1023,7 @@
     1.4    need to be passed-through carefully by syntax transformations.
     1.5  
     1.6    Pre-terms are further processed by the so-called \emph{check} and
     1.7 -  \emph{unckeck} phases that are intertwined with type-inference (see
     1.8 +  \emph{uncheck} phases that are intertwined with type-inference (see
     1.9    also @{cite "isabelle-implementation"}).  The latter allows to operate
    1.10    on higher-order abstract syntax with proper binding and type
    1.11    information already available.