'primitive' is not an adverb
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 552542bc951e6761a
parent 55253 cfd276a7dbeb
child 55255 eceebcea3e00
'primitive' is not an adverb
src/Doc/Datatypes/Datatypes.thy
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -1115,7 +1115,7 @@
     1.4    \qquad @{thm at_simps(2)[no_vars]}\]
     1.5  %
     1.6  The next example is defined using \keyw{fun} to escape the syntactic
     1.7 -restrictions imposed on primitive recursive functions. The
     1.8 +restrictions imposed on primitively recursive functions. The
     1.9  @{command datatype_new_compat} command is needed to register new-style datatypes
    1.10  for use with \keyw{fun} and \keyw{function}
    1.11  (Section~\ref{sssec:datatype-new-compat}):