# HG changeset patch
# User wenzelm
# Date 863023032 -7200
# Node ID 6c0c7e99312dd84ffc8483c0a82fd135c7f92609
# Parent  786faf45f1f3a359d1f1bd04e8c1901e08748a33
replaced Int by IntPr, result by qed;

diff -r 786faf45f1f3 -r 6c0c7e99312d doc-src/Logics/FOL.tex
--- 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}