--- a/ProgTutorial/Advanced.thy	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Advanced.thy	Sun Nov 22 15:27:10 2009 +0100
@@ -6,7 +6,7 @@
 setup{*
 open_file_with_prelude 
   "Advanced_Code.thy"
-  ["theory General", "imports Base FirstSteps", "begin"]
+  ["theory Advanced", "imports Base FirstSteps", "begin"]
 *}
 (*>*)
 
@@ -29,7 +29,7 @@
 section {* Theories\label{sec:theories} (TBD) *}
 
 text {*
-  As said above, theories are the most basic layer in Isabelle. They contain
+  Theories, as said above, are the most basic layer in Isabelle. They contain
   definitions, syntax declarations, axioms, proofs etc. If a definition is
   stated, it must be stored in a theory in order to be usable later
   on. Similar with proofs: once a proof is finished, the proved theorem needs

--- a/ProgTutorial/Essential.thy	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Essential.thy	Sun Nov 22 15:27:10 2009 +0100
@@ -6,7 +6,7 @@
 setup{*
 open_file_with_prelude 
   "Essential_Code.thy"
-  ["theory General", "imports Base FirstSteps", "begin"]
+  ["theory Essential", "imports Base FirstSteps", "begin"]
 *}
 (*>*)
 
@@ -1644,9 +1644,6 @@
   "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
   "True = False"}
 
-  The function @{ML make_thm in Skip_Proof} however only works if 
-  the ``quick-and-dirty'' mode is switched on. 
-
   Theorems also contain auxiliary data, such as the name of the theorem, its
   kind, the names for cases and so on. This data is stored in a string-string
   list and can be retrieved with the function @{ML_ind get_tags in

--- a/ProgTutorial/FirstSteps.thy	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Sun Nov 22 15:27:10 2009 +0100
@@ -893,7 +893,7 @@
 *}
 
 local_setup %gray {* 
-  Local_Theory.define "" ((@{binding "TrueConj"}, NoSyn), 
+  Local_Theory.define ((@{binding "TrueConj"}, NoSyn), 
       (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
 
 text {* 

--- a/ProgTutorial/Package/Ind_Code.thy	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Nov 22 15:27:10 2009 +0100
@@ -28,43 +28,17 @@
 ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy =
 let 
   val arg = ((predname, mx), (Attrib.empty_binding, trm))
-  val ((_, (_ , thm)), lthy') = Local_Theory.define "" arg lthy
+  val ((_, (_ , thm)), lthy') = Local_Theory.define arg lthy
 in 
   (thm, lthy') 
 end*}
 
 text {*
   It returns the definition (as a theorem) and the local theory in which the
-  definition has been made. In Line 4, the string @{ML "\"\""} is a flag
-  attached to the theorem (other possibile flags are @{ML_ind  definitionK in Thm}
-  and @{ML_ind theoremK in Thm}).\footnote{\bf FIXME: move to theorem section.} 
-  These flags just classify theorems and have no
-  significant meaning, except for tools that, for example, find theorems in
-  the theorem database.\footnote{FIXME: put in the section about theorems.} We
-  also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for
-  our inductive predicates are not meant to be seen by the user and therefore
-  do not need to have any theorem attributes. A testcase for this function is
-*}
-
-local_setup %gray {* fn lthy =>
-let
-  val arg = ((@{binding "My_True"}, NoSyn), @{term True})
-  val (def, lthy') = make_defn arg lthy 
-in
-  tracing (string_of_thm_no_vars lthy' def); lthy'
-end *}
-
-text {*
-  which introduces the definition @{thm My_True_def} and then prints it out. 
-  Since we are testing the function inside \isacommand{local\_setup}, i.e., make
-  actual changes to the ambient theory, we can query the definition with the usual
-  command \isacommand{thm}:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{thm [source] "My_True_def"}\\
-  @{text ">"}~@{thm "My_True_def"}
-  \end{isabelle}
-
+  definition has been made. We use @{ML_ind empty_binding in Attrib} in Line 3, 
+  since the definitions for our inductive predicates are not meant to be seen 
+  by the user and therefore do not need to have any theorem attributes. 
+ 
   The next two functions construct the right-hand sides of the definitions, 
   which are terms whose general form is:
 

--- a/ProgTutorial/Package/simple_inductive_package.ML	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Sun Nov 22 15:27:10 2009 +0100
@@ -22,7 +22,7 @@
 fun make_defs ((binding, syn), trm) lthy =
 let 
   val arg = ((binding, syn), (Attrib.empty_binding, trm))
-  val ((_, (_ , thm)), lthy) = Local_Theory.define "" arg lthy
+  val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy
 in 
   (thm, lthy) 
 end

--- 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.
 *}

Binary file progtutorial.pdf has changed