doc-src/ZF/FOL.tex
changeset 9695 ec7d7f877712
parent 8249 3fc32155372c
child 14154 3bc0128e2c74
     1.1 --- a/doc-src/ZF/FOL.tex	Mon Aug 28 13:50:24 2000 +0200
     1.2 +++ b/doc-src/ZF/FOL.tex	Mon Aug 28 13:52:38 2000 +0200
     1.3 @@ -192,7 +192,7 @@
     1.4  
     1.5  
     1.6  \section{Generic packages}
     1.7 -\FOL{} instantiates most of Isabelle's generic packages.
     1.8 +FOL instantiates most of Isabelle's generic packages.
     1.9  \begin{itemize}
    1.10  \item 
    1.11  It instantiates the simplifier.  Both equality ($=$) and the biconditional
    1.12 @@ -210,9 +210,9 @@
    1.13  It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
    1.14  for details. 
    1.15  
    1.16 -\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
    1.17 -  for an equality throughout a subgoal and its hypotheses.  This tactic uses
    1.18 -  \FOL's general substitution rule.
    1.19 +\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for
    1.20 +  an equality throughout a subgoal and its hypotheses.  This tactic uses FOL's
    1.21 +  general substitution rule.
    1.22  \end{itemize}
    1.23  
    1.24  \begin{warn}\index{simplification!of conjunctions}%
    1.25 @@ -331,10 +331,10 @@
    1.26  the rule
    1.27  $$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$
    1.28  \noindent
    1.29 -Natural deduction in classical logic is not really all that natural.
    1.30 -{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
    1.31 -well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
    1.32 -rule (see Fig.\ts\ref{fol-cla-derived}).
    1.33 +Natural deduction in classical logic is not really all that natural.  FOL
    1.34 +derives classical introduction rules for $\disj$ and~$\exists$, as well as
    1.35 +classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see
    1.36 +Fig.\ts\ref{fol-cla-derived}).
    1.37  
    1.38  The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
    1.39  Best_tac} refer to the default claset (\texttt{claset()}), which works for most
    1.40 @@ -897,8 +897,8 @@
    1.41  while~$R$ and~$A$ are true.  This truth assignment reduces the main goal to
    1.42  $true\bimp false$, which is of course invalid.
    1.43  
    1.44 -We can repeat this analysis by expanding definitions, using just
    1.45 -the rules of {\FOL}:
    1.46 +We can repeat this analysis by expanding definitions, using just the rules of
    1.47 +FOL:
    1.48  \begin{ttbox}
    1.49  choplev 0;
    1.50  {\out Level 0}