--- a/ProgTutorial/Tactical.thy	Tue Mar 24 12:09:38 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Mar 24 18:06:20 2009 +0100
@@ -347,7 +347,7 @@
 (*<*)oops(*>*)
 
 text {*
-  A simple tactic making theorem proving particularly simple is 
+  A simple tactic for ``easily'' discharging proof obligations is 
   @{ML SkipProof.cheat_tac}. This tactic corresponds to
   the Isabelle command \isacommand{sorry} and is sometimes useful  
   during the development of tactics.