summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/Intro/getting.tex

changeset 9695 | ec7d7f877712 |

parent 5205 | 602354039306 |

child 14148 | 6580d374a509 |

1.1 --- a/doc-src/Intro/getting.tex Mon Aug 28 13:50:24 2000 +0200 1.2 +++ b/doc-src/Intro/getting.tex Mon Aug 28 13:52:38 2000 +0200 1.3 @@ -26,7 +26,7 @@ 1.4 isabelle FOL 1.5 \end{ttbox} 1.6 Note that just typing \texttt{isabelle} usually brings up higher-order logic 1.7 -(\HOL) by default. 1.8 +(HOL) by default. 1.9 1.10 1.11 \subsection{Lexical matters} 1.12 @@ -110,8 +110,8 @@ 1.13 t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)} 1.14 \end{array} 1.15 \] 1.16 -Note that \HOL{} uses its traditional ``higher-order'' syntax for application, 1.17 -which differs from that used in \FOL\@. 1.18 +Note that HOL uses its traditional ``higher-order'' syntax for application, 1.19 +which differs from that used in FOL. 1.20 1.21 The theorems and rules of an object-logic are represented by theorems in 1.22 the meta-logic, which are expressed using meta-formulae. Since the 1.23 @@ -228,10 +228,10 @@ 1.24 to have subscript zero, improving readability and reducing subscript 1.25 growth. 1.26 \end{ttdescription} 1.27 -The rules of a theory are normally bound to \ML\ identifiers. Suppose we 1.28 -are running an Isabelle session containing theory~\FOL, natural deduction 1.29 -first-order logic.\footnote{For a listing of the \FOL{} rules and their 1.30 - \ML{} names, turn to 1.31 +The rules of a theory are normally bound to \ML\ identifiers. Suppose we are 1.32 +running an Isabelle session containing theory~FOL, natural deduction 1.33 +first-order logic.\footnote{For a listing of the FOL rules and their \ML{} 1.34 + names, turn to 1.35 \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}% 1.36 {page~\pageref{fol-rules}}.} 1.37 Let us try an example given in~\S\ref{joining}. We