diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Tactical.thy --- 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. *}