# HG changeset patch
# User lcp
# Date 773944017 -7200
# Node ID 03b445551763027d3bc1bce26bec815564f5985f
# Parent  877704b91847d3d5b36f1cec3349c7137dee12ab
minor edits

diff -r 877704b91847 -r 03b445551763 doc-src/Intro/advanced.tex
--- 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$:
diff -r 877704b91847 -r 03b445551763 doc-src/Intro/theorems.txt
--- 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);