
diff -r d69214e47ef9 -r efb5fff99c96 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Aug 20 23:30:51 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Fri Aug 21 11:42:14 2009 +0200
@@ -49,41 +49,43 @@
       THEN atac 1)
 end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
   
-  To start the proof, the function @{ML "Goal.prove"}~@{text "ctxt xs As C
-  tac"} sets up a goal state for proving the goal @{text C} 
-  (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the
-  assumptions @{text As} (happens to be empty) with the variables
-  @{text xs} that will be generalised once the goal is proved (in our case
-  @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
-  it can make use of the local assumptions (there are none in this example). 
-  The tactics @{ML_ind  etac}, @{ML_ind  rtac} and @{ML_ind  atac} 
-  in the code above correspond 
-  roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. 
-  The operator @{ML_ind  THEN} strings the tactics together. 
+  To start the proof, the function @{ML_ind "Goal.prove"}~@{text "ctxt xs As C
+  tac"} sets up a goal state for proving the goal @{text C} (that is @{prop "P
+  \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the assumptions @{text As}
+  (happens to be empty) with the variables @{text xs} that will be generalised
+  once the goal is proved (in our case @{text P} and @{text
+  Q}).\footnote{FIXME: explain prove earlier} The @{text "tac"} is the tactic
+  that proves the goal; it can make use of the local assumptions (there are
+  none in this example). The tactics @{ML_ind etac}, @{ML_ind rtac} and
+  @{ML_ind atac} in the code above correspond roughly to @{text erule}, @{text
+  rule} and @{text assumption}, respectively. The operator @{ML_ind THEN}
+  strings the tactics together.
 
   \begin{readmore}
-  To learn more about the function @{ML_ind  prove in Goal} see \isccite{sec:results}
-  and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
+  To learn more about the function @{ML_ind prove in Goal} see
+  \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
   "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
   tactics and tactic combinators; see also Chapters 3 and 4 in the old
-  Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. 
+  Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation
+  Manual.
   \end{readmore}
 
-  Note that in the code above we use antiquotations for referencing the theorems. Many theorems
-  also have ML-bindings with the same name. Therefore, we could also just have
-  written @{ML "etac disjE 1"}, or in case where there is no ML-binding obtain
-  the theorem dynamically using the function @{ML thm}; for example 
-  \mbox{@{ML  "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style! 
-  The reason
-  is that the binding for @{ML disjE} can be re-assigned by the user and thus
-  one does not have complete control over which theorem is actually
-  applied. This problem is nicely prevented by using antiquotations, because
-  then the theorems are fixed statically at compile-time.
+  Note that in the code above we use antiquotations for referencing the
+  theorems. Many theorems also have ML-bindings with the same name. Therefore,
+  we could also just have written @{ML "etac disjE 1"}, or in case where there
+  is no ML-binding obtain the theorem dynamically using the function @{ML
+  thm}; for example \mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however
+  are considered bad style! The reason is that the binding for @{ML disjE} can
+  be re-assigned by the user and thus one does not have complete control over
+  which theorem is actually applied. This problem is nicely prevented by using
+  antiquotations, because then the theorems are fixed statically at
+  compile-time.
 
-  During the development of automatic proof procedures, you will often find it 
-  necessary to test a tactic on examples. This can be conveniently 
-  done with the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
+  During the development of automatic proof procedures, you will often find it
+  necessary to test a tactic on examples. This can be conveniently done with
+  the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. 
   Consider the following sequence of tactics
+
 *}
 
 ML{*val foo_tac = 
@@ -302,7 +304,6 @@
   \end{figure}
 *}
 
-
 text {*
   which prints out the given theorem (using the string-function defined in
   Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. With this
@@ -315,9 +316,7 @@
   where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are
   the subgoals. So after setting up the lemma, the goal state is always of the
   form @{text "C \<Longrightarrow> #C"}; when the proof is finished we are left with @{text
-  "#C"}.\footnote{This only applies to single statements. If the lemma
-  contains more than one statement, then one has more such implications.} 
-  Since the goal @{term C} can potentially be an implication, there is a
+  "#C"}. Since the goal @{term C} can potentially be an implication, there is a
   ``protector'' wrapped around it (the wrapper is the outermost constant
   @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; in the figure we make it visible
   as an @{text #}). This wrapper prevents that premises of @{text C} are
@@ -1267,6 +1266,7 @@
   simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
 
+
 text {* 
   To see how they work, consider the function in Figure~\ref{fig:printss}, which
   prints out some parts of a simpset. If you use it to print out the components of the




