--- a/ProgTutorial/Tactical.thy	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Sun Nov 22 15:27:10 2009 +0100
@@ -429,15 +429,6 @@
 (*<*)oops(*>*)
 
 text {*
-  This tactic works however only if the quick-and-dirty mode of Isabelle 
-  is switched on. This is done automatically in the ``interactive
-  mode'' of Isabelle, but must be done manually in the ``batch mode''
-  with the assignment
-*}
-
-ML{*quick_and_dirty := true*}
-
-text {*
   Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown 
   earlier, corresponds to the assumption method.
 *}