doc-src/TutorialI/Types/numerics.tex
changeset 11428 332347b9b942
parent 11416 91886738773a
child 11480 0fba0357c04c
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Mon Jul 16 13:14:19 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Tue Jul 17 13:46:21 2001 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  \end{warn}
     1.5  
     1.6  \begin{warn}
     1.7 -\index{recdef@\protect\isacommand{recdef} (command)!and numeric literals}  
     1.8 +\index{recdef@\isacommand {recdef} (command)!and numeric literals}  
     1.9  Numeric literals are not constructors and therefore
    1.10  must not be used in patterns.  For example, this declaration is
    1.11  rejected:
    1.12 @@ -434,7 +434,7 @@
    1.13  Type \isa{real} is only available in the logic HOL-Real, which
    1.14  is  HOL extended with the rather substantial development of the real
    1.15  numbers.  Base your theory upon theory
    1.16 -\isa{Real}, not the usual \isa{Main}.%
    1.17 +\thydx{Real}, not the usual \isa{Main}.%
    1.18  \index{real numbers|)}\index{*real (type)|)}
    1.19  Launch Isabelle using the command 
    1.20  \begin{verbatim}