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

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}