--- a/doc-src/Logics/FOL.tex Wed May 07 18:36:13 1997 +0200
+++ b/doc-src/Logics/FOL.tex Wed May 07 18:37:12 1997 +0200
@@ -28,7 +28,7 @@
The unique existence quantifier, $\exists!x.P(x)$, is defined in terms
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
-quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates
+quantifications. For instance, $\exists!x\;y.P(x,y)$ abbreviates
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
@@ -255,16 +255,16 @@
for first-order logic because they discard universally quantified
assumptions after a single use.
\begin{ttbox}
-mp_tac : int -> tactic
-eq_mp_tac : int -> tactic
-Int.safe_step_tac : int -> tactic
-Int.safe_tac : tactic
-Int.inst_step_tac : int -> tactic
-Int.step_tac : int -> tactic
-Int.fast_tac : int -> tactic
-Int.best_tac : int -> tactic
+mp_tac : int -> tactic
+eq_mp_tac : int -> tactic
+IntPr.safe_step_tac : int -> tactic
+IntPr.safe_tac : tactic
+IntPr.inst_step_tac : int -> tactic
+IntPr.step_tac : int -> tactic
+IntPr.fast_tac : int -> tactic
+IntPr.best_tac : int -> tactic
\end{ttbox}
-Most of these belong to the structure {\tt Int} and resemble the
+Most of these belong to the structure {\tt IntPr} and resemble the
tactics of Isabelle's classical reasoner.
\begin{ttdescription}
@@ -280,27 +280,27 @@
is like {\tt mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
is safe.
-\item[\ttindexbold{Int.safe_step_tac} $i$] performs a safe step on
+\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
subgoal~$i$. This may include proof by assumption or Modus Ponens (taking
care not to instantiate unknowns), or {\tt hyp_subst_tac}.
-\item[\ttindexbold{Int.safe_tac}] repeatedly performs safe steps on all
+\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all
subgoals. It is deterministic, with at most one outcome.
-\item[\ttindexbold{Int.inst_step_tac} $i$] is like {\tt safe_step_tac},
+\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like {\tt safe_step_tac},
but allows unknowns to be instantiated.
-\item[\ttindexbold{Int.step_tac} $i$] tries {\tt safe_tac} or {\tt
+\item[\ttindexbold{IntPr.step_tac} $i$] tries {\tt safe_tac} or {\tt
inst_step_tac}, or applies an unsafe rule. This is the basic step of
the intuitionistic proof procedure.
-\item[\ttindexbold{Int.fast_tac} $i$] applies {\tt step_tac}, using
+\item[\ttindexbold{IntPr.fast_tac} $i$] applies {\tt step_tac}, using
depth-first search, to solve subgoal~$i$.
-\item[\ttindexbold{Int.best_tac} $i$] applies {\tt step_tac}, using
+\item[\ttindexbold{IntPr.best_tac} $i$] applies {\tt step_tac}, using
best-first search (guided by the size of the proof state) to solve subgoal~$i$.
\end{ttdescription}
-Here are some of the theorems that {\tt Int.fast_tac} proves
+Here are some of the theorems that {\tt IntPr.fast_tac} proves
automatically. The latter three date from {\it Principia Mathematica}
(*11.53, *11.55, *11.61)~\cite{principia}.
\begin{ttbox}
@@ -437,14 +437,14 @@
{\out No subgoals!}
\end{ttbox}
The theorem was proved in six tactic steps, not counting the abandoned
-ones. But proof checking is tedious; \ttindex{Int.fast_tac} proves the
+ones. But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
theorem in one step.
\begin{ttbox}
goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
{\out Level 0}
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out 1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
-by (Int.fast_tac 1);
+by (IntPr.fast_tac 1);
{\out Level 1}
{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
{\out No subgoals!}
@@ -525,7 +525,7 @@
{\out ~ ~ ((P --> Q) | (Q --> P))}
{\out No subgoals!}
\end{ttbox}
-This proof is also trivial for {\tt Int.fast_tac}.
+This proof is also trivial for {\tt IntPr.fast_tac}.
\section{A classical example} \label{fol-cla-example}
@@ -678,7 +678,7 @@
{\out Level 1}
{\out if(P,Q,R)}
{\out No subgoals!}
-val ifI = result();
+qed "ifI";
\end{ttbox}
@@ -706,7 +706,7 @@
{\out Level 2}
{\out S}
{\out No subgoals!}
-val ifE = result();
+qed "ifE";
\end{ttbox}
As you may recall from
\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
@@ -868,7 +868,7 @@
{\out by: tactic failed}
\end{ttbox}
This failure message is uninformative, but we can get a closer look at the
-situation by applying \ttindex{step_tac}.
+situation by applying \ttindex{Step_tac}.
\begin{ttbox}
by (REPEAT (Step_tac 1));
{\out Level 1}