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!}
2.1 --- a/doc-src/Intro/intro.ind Tue May 06 13:43:54 1997 +0200
2.2 +++ b/doc-src/Intro/intro.ind Tue May 06 13:49:29 1997 +0200
2.3 @@ -20,7 +20,7 @@
2.4 \item {\tt allI} theorem, 37
2.5 \item arities
2.6 \subitem declaring, 4, \bold{49}
2.7 - \item {\tt asm_simp_tac}, 60
2.8 + \item {\tt Asm_simp_tac}, 60
2.9 \item {\tt assume_tac}, 30, 32, 37, 47
2.10 \item assumptions
2.11 \subitem deleting, 20
2.12 @@ -207,7 +207,7 @@
2.13 \item search
2.14 \subitem depth-first, 63
2.15 \item signatures, \bold{9}
2.16 - \item {\tt simp_tac}, 60
2.17 + \item {\tt Simp_tac}, 60
2.18 \item simplification, 59
2.19 \item simplification sets, 59
2.20 \item sort constraints, 25