--- a/ProgTutorial/Tactical.thy	Thu Mar 19 23:21:26 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Sat Mar 21 12:35:03 2009 +0100
@@ -347,6 +347,20 @@
 (*<*)oops(*>*)
 
 text {*
+  A simple tactic making theorem proving particularly simple is 
+  @{ML SkipProof.cheat_tac}. This tactic corresponds to
+  the Isabelle command \isacommand{sorry} and is sometimes useful  
+  during the development of tactics.
+*}
+
+lemma shows "False" and "something_else_obviously_false"  
+apply(tactic {* SkipProof.cheat_tac @{theory} *})
+txt{*\begin{minipage}{\textwidth}
+     @{subgoals [display]}
+     \end{minipage}*}
+(*<*)oops(*>*)
+
+text {*
   Another simple tactic is the function @{ML atac}, which, as shown in the previous
   section, corresponds to the assumption command.
 *}