# HG changeset patch
# User wenzelm
# Date 862919369 -7200
# Node ID 943f25285a3eac6078094cebf7e2d450ca54572a
# Parent  a02abeafca6767ef928cce668fdd3067d4df27ba
fixed simplifier ex;

diff -r a02abeafca67 -r 943f25285a3e doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Tue May 06 13:43:54 1997 +0200
+++ b/doc-src/Intro/advanced.tex	Tue May 06 13:49:29 1997 +0200
@@ -1024,14 +1024,14 @@
 
 \index{simplification}\index{examples!of simplification} 
 
-Isabelle's simplification tactics repeatedly apply equations to a subgoal,
-perhaps proving it.  For efficiency, the rewrite rules must be
-packaged into a {\bf simplification set},\index{simplification sets} 
-or {\bf simpset}.  We take the standard simpset for first-order logic and
-insert the equations proved in the previous section, namely
-$0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$:
+Isabelle's simplification tactics repeatedly apply equations to a
+subgoal, perhaps proving it.  For efficiency, the rewrite rules must
+be packaged into a {\bf simplification set},\index{simplification
+  sets} or {\bf simpset}.  We augment the implicit simpset of {\FOL}
+with 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 addsimps [add_0, add_Suc];
+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$:
@@ -1049,10 +1049,10 @@
 {\out          Suc(x) + m + n = Suc(x) + (m + n)}
 \end{ttbox}
 The base case holds easily; both sides reduce to $m+n$.  The
-tactic~\ttindex{simp_tac} rewrites with respect to the given simplification
-set, applying the rewrite rules for addition:
+tactic~\ttindex{Simp_tac} rewrites with respect to the current
+simplification set, applying the rewrite rules for addition:
 \begin{ttbox}
-by (simp_tac add_ss 1);
+by (Simp_tac 1);
 {\out Level 2}
 {\out k + m + n = k + (m + n)}
 {\out  1. !!x. x + m + n = x + (m + n) ==>}
@@ -1060,10 +1060,10 @@
 \end{ttbox}
 The inductive step requires rewriting by the equations for addition
 together the induction hypothesis, which is also an equation.  The
-tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any
-useful assumptions:
+tactic~\ttindex{Asm_simp_tac} rewrites using the implicit
+simplification set and any useful assumptions:
 \begin{ttbox}
-by (asm_simp_tac add_ss 1);
+by (Asm_simp_tac 1);
 {\out Level 3}
 {\out k + m + n = k + (m + n)}
 {\out No subgoals!}
diff -r a02abeafca67 -r 943f25285a3e doc-src/Intro/intro.ind
--- a/doc-src/Intro/intro.ind	Tue May 06 13:43:54 1997 +0200
+++ b/doc-src/Intro/intro.ind	Tue May 06 13:49:29 1997 +0200
@@ -20,7 +20,7 @@
   \item {\tt allI} theorem, 37
   \item arities
     \subitem declaring, 4, \bold{49}
-  \item {\tt asm_simp_tac}, 60
+  \item {\tt Asm_simp_tac}, 60
   \item {\tt assume_tac}, 30, 32, 37, 47
   \item assumptions
     \subitem deleting, 20
@@ -207,7 +207,7 @@
   \item search
     \subitem depth-first, 63
   \item signatures, \bold{9}
-  \item {\tt simp_tac}, 60
+  \item {\tt Simp_tac}, 60
   \item simplification, 59
   \item simplification sets, 59
   \item sort constraints, 25