summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/ZF/FOL.tex

changeset 14158 | 15bab630ae31 |

parent 14154 | 3bc0128e2c74 |

child 30099 | dde11464969c |

--- a/doc-src/ZF/FOL.tex Wed Aug 20 11:12:48 2003 +0200 +++ b/doc-src/ZF/FOL.tex Wed Aug 20 13:05:22 2003 +0200 @@ -259,8 +259,9 @@ IntPr.fast_tac : int -> tactic IntPr.best_tac : int -> tactic \end{ttbox} -Most of these belong to the structure \ML{} \texttt{IntPr} and resemble the -tactics of Isabelle's classical reasoner. Note that you can use the +Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the +tactics of Isabelle's classical reasoner. There are no corresponding +Isar methods, but you can use the \isa{tactic} method to call \ML{} tactics in an Isar script: \begin{isabelle} \isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*}) @@ -350,12 +351,14 @@ \section{An intuitionistic example} -Here is a session similar to one in {\em Logic and Computation} -\cite[pages~222--3]{paulson87}. Isabelle treats quantifiers differently -from {\sc lcf}-based theorem provers such as {\sc hol}. +Here is a session similar to one in the book {\em Logic and Computation} +\cite[pages~222--3]{paulson87}. It illustrates the treatment of +quantifier reasoning, which is different in Isabelle than it is in +{\sc lcf}-based theorem provers such as {\sc hol}. -The theory header must specify that we are working in intuitionistic -logic: +The theory header specifies that we are working in intuitionistic +logic by designating \isa{IFOL} rather than \isa{FOL} as the parent +theory: \begin{isabelle} \isacommand{theory}\ IFOL\_examples\ =\ IFOL: \end{isabelle} @@ -524,7 +527,7 @@ $\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise $\all{x}P(x)$ is true. Either way the theorem holds. First, we must -work in a theory based on classical logic: +work in a theory based on classical logic, the theory \isa{FOL}: \begin{isabelle} \isacommand{theory}\ FOL\_examples\ =\ FOL: \end{isabelle}