1.1 --- a/doc-src/Intro/advanced.tex	Mon Jul 11 17:50:34 1994 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Mon Jul 11 18:26:57 1994 +0200
     1.3 @@ -864,14 +864,14 @@
     1.4  \begin{ttbox}
     1.5  goal Nat.thy "~ (Suc(k) = k)";
     1.6  {\out Level 0}
     1.7 -{\out ~Suc(k) = k}
     1.8 -{\out  1. ~Suc(k) = k}
     1.9 +{\out Suc(k) ~= k}
    1.10 +{\out  1. Suc(k) ~= k}
    1.11  \ttbreak
    1.12  by (res_inst_tac [("n","k")] induct 1);
    1.13  {\out Level 1}
    1.14 -{\out ~Suc(k) = k}
    1.15 -{\out  1. ~Suc(0) = 0}
    1.16 -{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
    1.17 +{\out Suc(k) ~= k}
    1.18 +{\out  1. Suc(0) ~= 0}
    1.19 +{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
    1.20  \end{ttbox}
    1.21  We should check that Isabelle has correctly applied induction.  Subgoal~1
    1.22  is the base case, with $k$ replaced by~0.  Subgoal~2 is the inductive step,
    1.23 @@ -881,14 +881,14 @@
    1.24  \begin{ttbox}
    1.25  by (resolve_tac [notI] 1);
    1.26  {\out Level 2}
    1.27 -{\out ~Suc(k) = k}
    1.28 +{\out Suc(k) ~= k}
    1.29  {\out  1. Suc(0) = 0 ==> False}
    1.30 -{\out  2. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
    1.31 +{\out  2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
    1.32  \ttbreak
    1.33  by (eresolve_tac [Suc_neq_0] 1);
    1.34  {\out Level 3}
    1.35 -{\out ~Suc(k) = k}
    1.36 -{\out  1. !!x. ~Suc(x) = x ==> ~Suc(Suc(x)) = Suc(x)}
    1.37 +{\out Suc(k) ~= k}
    1.38 +{\out  1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)}
    1.39  \end{ttbox}
    1.40  The inductive step holds by the contrapositive of~\ttindex{Suc_inject}.
    1.41  Negation rules transform the subgoal into that of proving $Suc(x)=x$ from
    1.42 @@ -896,17 +896,17 @@
    1.43  \begin{ttbox}
    1.44  by (resolve_tac [notI] 1);
    1.45  {\out Level 4}
    1.46 -{\out ~Suc(k) = k}
    1.47 -{\out  1. !!x. [| ~Suc(x) = x; Suc(Suc(x)) = Suc(x) |] ==> False}
    1.48 +{\out Suc(k) ~= k}
    1.49 +{\out  1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False}
    1.50  \ttbreak
    1.51  by (eresolve_tac [notE] 1);
    1.52  {\out Level 5}
    1.53 -{\out ~Suc(k) = k}
    1.54 +{\out Suc(k) ~= k}
    1.55  {\out  1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x}
    1.56  \ttbreak
    1.57  by (eresolve_tac [Suc_inject] 1);
    1.58  {\out Level 6}
    1.59 -{\out ~Suc(k) = k}
    1.60 +{\out Suc(k) ~= k}
    1.61  {\out No subgoals!}
    1.62  \end{ttbox}
    1.63  
    1.64 @@ -983,7 +983,7 @@
    1.65  insert the equations proved in the previous section, namely
    1.66  $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
    1.67  \begin{ttbox}
    1.68 -val add_ss = FOL_ss addrews [add_0, add_Suc];
    1.69 +val add_ss = FOL_ss addsimps [add_0, add_Suc];
    1.70  \end{ttbox}
    1.71  We state the goal for associativity of addition, and
    1.72  use \ttindex{res_inst_tac} to invoke induction on~$k$: