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

doc-src/ZF/FOL.tex

changeset 9695 | ec7d7f877712 |

parent 8249 | 3fc32155372c |

child 14154 | 3bc0128e2c74 |

--- a/doc-src/ZF/FOL.tex Mon Aug 28 13:50:24 2000 +0200 +++ b/doc-src/ZF/FOL.tex Mon Aug 28 13:52:38 2000 +0200 @@ -192,7 +192,7 @@ \section{Generic packages} -\FOL{} instantiates most of Isabelle's generic packages. +FOL instantiates most of Isabelle's generic packages. \begin{itemize} \item It instantiates the simplifier. Both equality ($=$) and the biconditional @@ -210,9 +210,9 @@ It instantiates the classical reasoner. See~\S\ref{fol-cla-prover} for details. -\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes - for an equality throughout a subgoal and its hypotheses. This tactic uses - \FOL's general substitution rule. +\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for + an equality throughout a subgoal and its hypotheses. This tactic uses FOL's + general substitution rule. \end{itemize} \begin{warn}\index{simplification!of conjunctions}% @@ -331,10 +331,10 @@ the rule $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$ \noindent -Natural deduction in classical logic is not really all that natural. -{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap -rule (see Fig.\ts\ref{fol-cla-derived}). +Natural deduction in classical logic is not really all that natural. FOL +derives classical introduction rules for $\disj$ and~$\exists$, as well as +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see +Fig.\ts\ref{fol-cla-derived}). The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works for most @@ -897,8 +897,8 @@ while~$R$ and~$A$ are true. This truth assignment reduces the main goal to $true\bimp false$, which is of course invalid. -We can repeat this analysis by expanding definitions, using just -the rules of {\FOL}: +We can repeat this analysis by expanding definitions, using just the rules of +FOL: \begin{ttbox} choplev 0; {\out Level 0}