doc-src/TutorialI/ToyList/ToyList.thy
changeset 10654 458068404143
parent 10362 c6b197ccf1f1
child 10790 520dd8696927
     1.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Wed Dec 13 09:32:55 2000 +0100
     1.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Dec 13 09:39:53 2000 +0100
     1.3 @@ -69,7 +69,8 @@
     1.4  \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
     1.5  particularly primitive kind where each recursive call peels off a datatype
     1.6  constructor from one of the arguments.  Thus the
     1.7 -recursion always terminates, i.e.\ the function is \bfindex{total}.
     1.8 +recursion always terminates, i.e.\ the function is \textbf{total}.
     1.9 +\index{total function}
    1.10  
    1.11  The termination requirement is absolutely essential in HOL, a logic of total
    1.12  functions. If we were to drop it, inconsistencies would quickly arise: the