--- a/CookBook/Tactical.thy	Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/Tactical.thy	Mon Mar 16 00:12:32 2009 +0100
@@ -1470,7 +1470,7 @@
 *}
 
 lemma shows "Suc 0 = 1"
-  apply(simp)
+apply(simp)
 (*<*)oops(*>*)
 
 text {*
@@ -1493,14 +1493,14 @@
 *}
 
 lemma shows "Suc 0 = 1"
-  apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail_sp}]) 1*})
 (*<*)oops(*>*)
 
 text {*
   Now the message shows up only once since the term @{term "1::nat"} is 
   left unchanged. 
 
-  Setting up a simproc using the command \isacommand{setup\_simproc} will
+  Setting up a simproc using the command \isacommand{simproc\_setup} will
   always add automatically the simproc to the current simpset. If you do not
   want this, then you have to use a slightly different method for setting 
   up the simproc. First the function @{ML fail_sp_aux} needs to be modified