--- a/ProgTutorial/Parsing.thy	Sat Apr 25 14:28:58 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sat Apr 25 17:46:47 2009 +0200
@@ -146,7 +146,7 @@
 in 
   (just_e input, just_h input)
 end"
-  "((\"e\", [\"l\", \"l\", \"o\"]),(\"h\", [\"l\", \"l\", \"o\"]))"}
+  "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
 
   The parser @{ML "Scan.optional p x" for p x} returns the result of the parser 
   @{text "p"}, if it succeeds; otherwise it returns 
@@ -424,7 +424,7 @@
  Token (\<dots>,(Space, \" \"),\<dots>), 
  Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
 
-  Many parsing functions later on will require spaces, comments and the like
+  Many parsing functions later on will require white space, comments and the like
   to have already been filtered out.  So from now on we are going to use the 
   functions @{ML filter} and @{ML OuterLex.is_proper} to do this. For example:
 
@@ -452,9 +452,8 @@
  Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
 
   you obtain a list consisting of only one command and two keyword tokens.
-  If you want to see which keywords and commands are currently known to Isabelle, type in
-  the following code (you might have to adjust the @{ML print_depth} in order to
-  see the complete list):
+  If you want to see which keywords and commands are currently known to Isabelle, 
+  type:
 
 @{ML_response_fake [display,gray] 
 "let 
@@ -464,6 +463,9 @@
 end" 
 "([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
 
+  You might have to adjust the @{ML print_depth} in order to
+  see the complete list.
+
   The parser @{ML "OuterParse.$$$"} parses a single keyword. For example:
 
 @{ML_response [display,gray]
@@ -579,12 +581,12 @@
   in which the @{text [quotes] "\\n"} causes the second token to be in 
   line 8.
 
-  By using the parser @{ML OuterParse.position} you can decode the positional
-  information and return it as part of the parsed input. For example
+  By using the parser @{ML OuterParse.position} you can access the token position
+  and return it as part of the parser result. For example
 
 @{ML_response_fake [display,gray]
 "let
-  val input = (filtered_input' \"where\")
+  val input = filtered_input' \"where\"
 in 
   parse (OuterParse.position (OuterParse.$$$ \"where\")) input
 end"
@@ -683,7 +685,7 @@
                (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
 text {*
-  Note that the parser does not parse the keyword \simpleinductive, even if it is
+  Note that the parser must not parse the keyword \simpleinductive, even if it is
   meant to process definitions as shown above. The parser of the keyword 
   will be given by the infrastructure that will eventually call @{ML spec_parser}.
   
@@ -734,12 +736,12 @@
   Whenever types are given, they are stored in the @{ML SOME}s. The types are
   not yet used to type the variables: this must be done by type-inference later
   on. Since types are part of the inner syntax they are strings with some
-  encoded information (see previous section). If a syntax translation is
+  encoded information (see previous section). If a mixfix-syntax is
   present for a variable, then it is stored in the @{ML Mixfix} data structure;
   no syntax translation is indicated by @{ML NoSyn}.
 
   \begin{readmore}
-  The data structure for syntax annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
+  The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
   \end{readmore}
 
   Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
@@ -858,9 +860,9 @@
   @{text "\<verbclose>"}\\
   \isacommand{end}
   \end{graybox}
-  \caption{The file @{text "Command.thy"} is necessary for generating a log 
-  file. This log file enables Isabelle to generate a keyword file containing 
-  the command \isacommand{foobar}.\label{fig:commandtheory}}
+  \caption{This file can be used to generate a log file. This log file in turn can
+  be used to generate a keyword file containing the command \isacommand{foobar}.
+  \label{fig:commandtheory}}
   \end{figure}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -909,7 +911,7 @@
   If the compilation succeeds, you have finally created all the necessary log files. 
   They are stored in the directory 
   
-  @{text [display]  "~/.isabelle/heaps/Isabelle2008/polyml-5.2.1_x86-linux/log"}
+  @{text [display]  "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"}
 
   or something similar depending on your Isabelle distribution and architecture.
   One quick way to assign a shell variable to this directory is by typing
@@ -937,7 +939,7 @@
   the string @{text "foobar"} twice.\footnote{To see whether things are fine, check
   that @{text "grep foobar"} on this file returns something
   non-empty.}  This keyword file needs to
-  be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle
+  be copied into the directory @{text "~/.isabelle/etc"}. To make ProofGeneral
   aware of this keyword file, you have to start Isabelle with the option @{text
   "-k foobar"}, that is:
 
@@ -1010,11 +1012,11 @@
 *}
 
 ML%linenosgray{*let
-  fun prove_prop str ctxt =
+  fun prove_prop str lthy =
     let
-      val prop = Syntax.read_prop ctxt str
+      val prop = Syntax.read_prop lthy str
     in
-      Proof.theorem_i NONE (K I) [[(prop,[])]] ctxt
+      Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
     end;
   
   val prove_prop_parser = OuterParse.prop >> prove_prop 
@@ -1052,7 +1054,8 @@
   \isacommand{done}
   \end{isabelle}
 
-  (FIXME: read a name and show how to store theorems)
+  (FIXME: read a name and show how to store theorems; see @{ML LocalTheory.note})
+  
 *}
 
 section {* Methods (TBD) *}
@@ -1075,20 +1078,20 @@
   An example of a very simple method is:
 *}
 
-method_setup %gray foobar_meth = 
+method_setup %gray foobar = 
  {* Scan.succeed
       (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
          "foobar method for conjE and conjI"
 
 text {*
-  It defines the method @{text foobar_meth}, which takes no arguments (therefore the
+  It defines the method @{text foobar}, which takes no arguments (therefore the
   parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which 
   applies @{thm [source] conjE} and then @{thm [source] conjI}. The function @{ML SIMPLE_METHOD}
-  turns such a tactic into a method. @{text "Foobar_meth"} can be used as follows
+  turns such a tactic into a method. The method @{text "foobar"} can be used as follows
 *}
 
 lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
-apply(foobar_meth)
+apply(foobar)
 txt {*
   where it results in the goal state
 

--- a/ProgTutorial/Tactical.thy	Sat Apr 25 14:28:58 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sat Apr 25 17:46:47 2009 +0200
@@ -56,8 +56,8 @@
   @{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 functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to 
-  @{text erule}, @{text rule} and @{text assumption}, respectively. 
+  The tactics @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond 
+  roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. 
   The operator @{ML THEN} strings the tactics together. 
 
   \begin{readmore}
@@ -145,7 +145,9 @@
   @{text "*** At command \"apply\"."}
   \end{isabelle}
 
-  This means they failed. The reason for this error message is that tactics 
+  This means they failed.\footnote{To be precise tactics do not produce this error
+  message, the it originates from the \isacommand{apply} wrapper.} The reason for this 
+  error message is that tactics 
   are functions mapping a goal state to a (lazy) sequence of successor states. 
   Hence the type of a tactic is:
 *}
@@ -310,10 +312,12 @@
   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)"}. 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)"}; however this constant
-  is invisible in the figure). This wrapper prevents that premises of @{text C} are
+  "(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
+  ``protector'' wrapped around it (the wrapper is the outermost constant
+  @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant is invisible
+  in the figure). This wrapper prevents that premises of @{text C} are
   misinterpreted as open subgoals. While tactics can operate on the subgoals
   (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion
   @{term C} intact, with the exception of possibly instantiating schematic
@@ -362,6 +366,9 @@
 (*<*)oops(*>*)
 
 text {*
+  This tactic works however only if the quick-and-dirty mode of Isabelle 
+  is switched on.
+
   Another simple tactic is the function @{ML atac}, which, as shown in the previous
   section, corresponds to the assumption command.
 *}
@@ -374,7 +381,7 @@
 (*<*)oops(*>*)
 
 text {*
-  Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond
+  Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond (roughly)
   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   respectively. Each of them take a theorem as argument and attempt to 
   apply it to a goal. Below are three self-explanatory examples.
@@ -461,7 +468,7 @@
   applied to the first subgoal might instantiate this meta-variable in such a 
   way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"}
   should be, then this situation can be avoided by introducing a more
-  constraint version of the @{text bspec}-rule. Such constraints can be given by
+  constrained version of the @{text bspec}-rule. Such constraints can be given by
   pre-instantiating theorems with other theorems. One function to do this is
   @{ML RS}
   
@@ -516,7 +523,7 @@
   Often proofs on the ML-level involve elaborate operations on assumptions and 
   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   shown so far is very unwieldy and brittle. Some convenience and
-  safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters 
+  safety is provided by @{ML SUBPROOF}. This tactic fixes the parameters 
   and binds the various components of a goal state to a record. 
   To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
   takes a record and just prints out the content of this record (using the 
@@ -629,20 +636,19 @@
 (*<*)oops(*>*)
 
 text {*
-  The restriction in this tactic which is not present in @{ML atac} is 
-  that it cannot instantiate any
-  schematic variable. This might be seen as a defect, but it is actually
-  an advantage in the situations for which @{ML SUBPROOF} was designed: 
-  the reason is that, as mentioned before, instantiation of schematic variables can affect 
-  several goals and can render them unprovable. @{ML SUBPROOF} is meant 
-  to avoid this.
+  The restriction in this tactic which is not present in @{ML atac} is that it
+  cannot instantiate any schematic variables. This might be seen as a defect,
+  but it is actually an advantage in the situations for which @{ML SUBPROOF}
+  was designed: the reason is that, as mentioned before, instantiation of
+  schematic variables can affect several goals and can render them
+  unprovable. @{ML SUBPROOF} is meant to avoid this.
 
-  Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with 
-  the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in 
-  the \isacommand{apply}-step uses @{text "1"}. This is another advantage 
-  of @{ML SUBPROOF}: the addressing  inside it is completely 
-  local to the tactic inside the subproof. It is therefore possible to also apply 
-  @{ML atac'} to the second goal by just writing:
+  Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
+  the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
+  the \isacommand{apply}-step uses @{text "1"}. This is another advantage of
+  @{ML SUBPROOF}: the addressing inside it is completely local to the tactic
+  inside the subproof. It is therefore possible to also apply @{ML atac'} to
+  the second goal by just writing:
 *}
 
 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"

Binary file progtutorial.pdf has changed