--- a/ProgTutorial/General.thy	Wed Oct 14 12:33:38 2009 +0200
+++ b/ProgTutorial/General.thy	Wed Oct 14 14:56:19 2009 +0200
@@ -857,6 +857,8 @@
   the theorem does not have any meta-variables that would be present if we proved
   this theorem on the user-level. We will see later on that usually we have to 
   construct meta-variables in theorems explicitly.
+
+  \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}}
 *}
 
 text {*
@@ -963,11 +965,11 @@
   a meta-equation between the given theorem and the theorem transformed
   into the object logic. The result is the theorem with object logic 
   connectives. However, in order to completely transform a theorem
-  such as @{thm [source] list.induct}
+  such as @{thm [source] list.induct}, which is of the form 
 
   @{thm [display] list.induct}
 
-  we have to first abstract over the variables @{text "?P"} and 
+  we have to first abstract over the meta variables @{text "?P"} and 
   @{text "?list"}. For this we can use the function 
   @{ML_ind forall_intr_vars in Drule}. 
 *}
@@ -981,7 +983,7 @@
 end*}
 
 text {*
-  For @{thm [source] list.induct} it produces:
+  For the theorem @{thm [source] list.induct}, this function produces:
 
   @{ML_response_fake [display, gray]
   "atomize_thm @{thm list.induct}"
@@ -989,7 +991,7 @@
 
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achive this is by using the function @{ML_ind prove in Goal}. 
-  For example
+  For example below we prove the term @{term "P \<Longrightarrow> P"}.
   
   @{ML_response_fake [display,gray]
   "let
@@ -1002,8 +1004,9 @@
 
   This function takes as second argument a list of strings. This list specifies
   which variables should be turned into meta-variables once the term is proved.
-  The proof is given in form of a tactic. We explain tactics in 
-  Chapter~\ref{chp:tactical}. 
+  The proof is given in form of a tactic as last argument. We explain tactics in 
+  Chapter~\ref{chp:tactical}. In the code above the tactic proved the theorem 
+  by assumption.
 
   Theorems also contain auxiliary data, such their names and kind, but also 
   names for cases etc. This data is stored in a string-string list and can
@@ -1020,7 +1023,8 @@
   "Thm.get_tags @{thm foo_data}"
   "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
 
-  We can extend the data associated with this lemma by attaching case names.  
+  When we store lemmas in the theorem database, we can explicitly extend the data 
+  associated with this lemma by attaching case names.  
 *}
 
 local_setup %gray {*
@@ -1030,22 +1034,42 @@
         @{thm foo_data})]) #> snd *}
 
 text {*
-  The date of the theorem @{thm [source] foo_data'} is as follows:
+  The data of the theorem @{thm [source] foo_data'} is then as follows:
 
   @{ML_response_fake [display,gray]
   "Thm.get_tags @{thm foo_data'}"
   "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), 
  (\"case_names\", \"foo_case1;foo_case2\")]"}
+
+  You notice the difference when using the proof methods @{ML_text cases} 
+  or @{ML_text induct}. In the proof below
 *}
 
 lemma
   "Q \<Longrightarrow> Q \<Longrightarrow> Q"
-proof (induct rule: foo_data')
+proof (cases rule: foo_data')
+print_cases
+(*<*)oops(*>*)
+
+text {*
+  we can proceed by analysing the cases @{ML_text "foo_case1"} and 
+  @{ML_text "foo_case2"}. While if the theorem has no names, then
+  the cases have standard names @{ML_text 1}, @{ML_text 2} and so 
+  on. This can be seen in the proof below.
+*}
+
+lemma
+  "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+proof (cases rule: foo_data)
+print_cases
 (*<*)oops(*>*)
 
 text {*
   TBD below
 
+  One great feature of Isabelle is its document preparation system where
+  proved theorems can be quoted in the text directly from the formalisation. 
+
   (FIXME: example for how to add theorem styles)
 *}
 
@@ -1068,11 +1092,12 @@
 strip_assums_all ([], @{term "\<And>x y. A x y"})
 *}
 
+(*
 setup %gray {*
   TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
   TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
 *}
-
+*)
 lemma 
   shows "A \<Longrightarrow> B"
   and   "C \<Longrightarrow> D"
@@ -1376,14 +1401,6 @@
 
 section {* Local Theories (TBD) *}
 
-section {* Storing Theorems\label{sec:storing} (TBD) *}
-
-text {* @{ML_ind  add_thms_dynamic in PureThy} *}
-
-local_setup %gray {* 
-  LocalTheory.note Thm.theoremK 
-    ((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
-
 
 (*
 setup {*
@@ -1738,5 +1755,15 @@
 
 section {* Managing Name Spaces (TBD) *}
 
+section {* Summary *}
+
+text {*
+  \begin{conventions}
+  \begin{itemize}
+  \item Start with a proper context and then pass it around 
+  through all your functions.
+  \end{itemize}
+  \end{conventions}
+*}
 
 end

--- a/ProgTutorial/Recipes/ExternalSolver.thy	Wed Oct 14 12:33:38 2009 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Wed Oct 14 14:56:19 2009 +0200
@@ -27,12 +27,10 @@
   properly. For example, the following expression takes only approximately
   one second:
 
-  @{ML_response [display,gray] 
+  @{ML_response_fake [display,gray] 
     "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
      handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
-*}
 
-text {*
   The function @{ML system_out} can also be used for more reasonable
   applications, e.g. coupling external solvers with Isabelle. In that case,
   one has to make sure that Isabelle can find the particular executable.

Binary file progtutorial.pdf has changed