--- a/doc-src/Intro/advanced.tex Mon Jul 11 17:50:34 1994 +0200
+++ b/doc-src/Intro/advanced.tex Mon Jul 11 18:26:57 1994 +0200
@@ -864,14 +864,14 @@
\begin{ttbox}
goal Nat.thy "~ (Suc(k) = k)";
{\out Level 0}
-{\out ~Suc(k) = k}
-{\out 1. ~Suc(k) = k}
+{\out Suc(k) ~= k}
+{\out 1. Suc(k) ~= k}
\ttbreak
by (res_inst_tac [("n","k")] induct 1);
{\out Level 1}
-{\out ~Suc(k) = k}
-{\out 1. ~Suc(0) = 0}
-{\out 2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
+{\out Suc(k) ~= k}
+{\out 1. Suc(0) ~= 0}
+{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
\end{ttbox}
We should check that Isabelle has correctly applied induction. Subgoal~1
is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step,
@@ -881,14 +881,14 @@
\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 2}
-{\out ~Suc(k) = k}
+{\out Suc(k) ~= k}
{\out 1. Suc(0) = 0 ==> False}
-{\out 2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
+{\out 2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
\ttbreak
by (eresolve_tac [Suc_neq_0] 1);
{\out Level 3}
-{\out ~Suc(k) = k}
-{\out 1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
+{\out Suc(k) ~= k}
+{\out 1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
\end{ttbox}
The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
@@ -896,17 +896,17 @@
\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 4}
-{\out ~Suc(k) = k}
-{\out 1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}
+{\out Suc(k) ~= k}
+{\out 1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
\ttbreak
by (eresolve_tac [notE] 1);
{\out Level 5}
-{\out ~Suc(k) = k}
+{\out Suc(k) ~= k}
{\out 1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
\ttbreak
by (eresolve_tac [Suc_inject] 1);
{\out Level 6}
-{\out ~Suc(k) = k}
+{\out Suc(k) ~= k}
{\out No subgoals!}
\end{ttbox}
@@ -983,7 +983,7 @@
insert the equations proved in the previous section, namely
$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
\begin{ttbox}
-val add_ss = FOL_ss addrews [add_0, add_Suc];
+val add_ss = FOL_ss addsimps [add_0, add_Suc];
\end{ttbox}
We state the goal for associativity of addition, and
use \ttindex{res_inst_tac} to invoke induction on~$k$:
--- a/doc-src/Intro/theorems.txt Mon Jul 11 17:50:34 1994 +0200
+++ b/doc-src/Intro/theorems.txt Mon Jul 11 18:26:57 1994 +0200
@@ -58,7 +58,7 @@
(*tactics *)
-goal cla_thy "P|P --> P";
+goal FOL.thy "P|P --> P";
by (resolve_tac [impI] 1);
by (resolve_tac [disjE] 1);
by (assume_tac 3);
@@ -67,7 +67,7 @@
val mythm = prth(result());
-goal cla_thy "(P & Q) | R --> (P | R)";
+goal FOL.thy "(P & Q) | R --> (P | R)";
by (resolve_tac [impI] 1);
by (eresolve_tac [disjE] 1);
by (dresolve_tac [conjunct1] 1);
@@ -76,7 +76,7 @@
by (REPEAT (assume_tac 1));
-- goal cla_thy "(P & Q) | R --> (P | R)";
+- goal FOL.thy "(P & Q) | R --> (P | R)";
Level 0
P & Q | R --> P | R
1. P & Q | R --> P | R
@@ -110,7 +110,7 @@
No subgoals!
-goal cla_thy "(P | Q) | R --> P | (Q | R)";
+goal FOL.thy "(P | Q) | R --> P | (Q | R)";
by (resolve_tac [impI] 1);
by (eresolve_tac [disjE] 1);
by (eresolve_tac [disjE] 1);