1.1 --- a/doc-src/Intro/advanced.tex	Tue May 06 13:43:54 1997 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Tue May 06 13:49:29 1997 +0200
     1.3 @@ -1024,14 +1024,14 @@
     1.4  
     1.5  \index{simplification}\index{examples!of simplification} 
     1.6  
     1.7 -Isabelle's simplification tactics repeatedly apply equations to a subgoal,
     1.8 -perhaps proving it.  For efficiency, the rewrite rules must be
     1.9 -packaged into a {\bf simplification set},\index{simplification sets} 
    1.10 -or {\bf simpset}.  We take the standard simpset for first-order logic and
    1.11 -insert the equations proved in the previous section, namely
    1.12 -$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
    1.13 +Isabelle's simplification tactics repeatedly apply equations to a
    1.14 +subgoal, perhaps proving it.  For efficiency, the rewrite rules must
    1.15 +be packaged into a {\bf simplification set},\index{simplification
    1.16 +  sets} or {\bf simpset}.  We augment the implicit simpset of {\FOL}
    1.17 +with the equations proved in the previous section, namely $0+n=n$ and
    1.18 +${\tt Suc}(m)+n={\tt Suc}(m+n)$:
    1.19  \begin{ttbox}
    1.20 -val add_ss = FOL_ss addsimps [add_0, add_Suc];
    1.21 +Addsimps [add_0, add_Suc];
    1.22  \end{ttbox}
    1.23  We state the goal for associativity of addition, and
    1.24  use \ttindex{res_inst_tac} to invoke induction on~$k$:
    1.25 @@ -1049,10 +1049,10 @@
    1.26  {\out          Suc(x) + m + n = Suc(x) + (m + n)}
    1.27  \end{ttbox}
    1.28  The base case holds easily; both sides reduce to $m+n$.  The
    1.29 -tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
    1.30 -set, applying the rewrite rules for addition:
    1.31 +tactic~\ttindex{Simp_tac} rewrites with respect to the current
    1.32 +simplification set, applying the rewrite rules for addition:
    1.33  \begin{ttbox}
    1.34 -by (simp_tac add_ss 1);
    1.35 +by (Simp_tac 1);
    1.36  {\out Level 2}
    1.37  {\out k + m + n = k + (m + n)}
    1.38  {\out  1. !!x. x + m + n = x + (m + n) ==>}
    1.39 @@ -1060,10 +1060,10 @@
    1.40  \end{ttbox}
    1.41  The inductive step requires rewriting by the equations for addition
    1.42  together the induction hypothesis, which is also an equation.  The
    1.43 -tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
    1.44 -useful assumptions:
    1.45 +tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
    1.46 +simplification set and any useful assumptions:
    1.47  \begin{ttbox}
    1.48 -by (asm_simp_tac add_ss 1);
    1.49 +by (Asm_simp_tac 1);
    1.50  {\out Level 3}
    1.51  {\out k + m + n = k + (m + n)}
    1.52  {\out No subgoals!}