--- a/ProgTutorial/Package/Ind_Code.thy	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Tue Mar 31 20:31:18 2009 +0100
@@ -1101,4 +1101,68 @@
 thm Even_def
 thm Odd_def
 
+text {* 
+  Second, we want that the user can specify fixed parameters.
+  Remember in the previous section we stated that the user can give the 
+  specification for the transitive closure of a relation @{text R} as 
+*}
+
+simple_inductive
+  trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "trcl\<iota>\<iota> R x x"
+| step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"
+
+text {*
+  Note that there is no locale given in this specification---the parameter
+  @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
+  stays fixed throughout the specification. The problem with this way of
+  stating the specification for the transitive closure is that it derives the
+  following induction principle.
+
+  \begin{center}\small
+  \mprset{flushleft}
+  \mbox{\inferrule{
+             @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
+             @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
+            {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
+  \end{center}
+
+  But this does not correspond to the induction principle we derived by hand, which
+  was
+  
+  \begin{center}\small
+  \mprset{flushleft}
+  \mbox{\inferrule{
+             @{thm_style prem1  trcl_induct[no_vars]}\\\\
+             @{thm_style prem2  trcl_induct[no_vars]}\\\\
+             @{thm_style prem3  trcl_induct[no_vars]}}
+            {@{thm_style concl  trcl_induct[no_vars]}}}  
+  \end{center}
+
+  The difference is that in the one derived by hand the relation @{term R} is not
+  a parameter of the proposition @{term P} to be proved and it is also not universally
+  qunatified in the second and third premise. The point is that the parameter @{term R}
+  stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''
+  argument of the transitive closure, but one that can be freely instantiated. 
+  In order to recognise such parameters, we have to extend the specification
+  to include a mechanism to state fixed parameters. The user should be able
+  to write 
+
+*}
+
+(*
+simple_inductive
+  trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "trcl'' R x x"
+| step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"
+
+simple_inductive
+  accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
+*)
+
 end

--- a/ProgTutorial/Package/Ind_Interface.thy	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy	Tue Mar 31 20:31:18 2009 +0100
@@ -7,19 +7,19 @@
 text {* 
   To be able to write down the specification in Isabelle, we have to introduce
   a new command (see Section~\ref{sec:newcommand}).  As the keyword for the
-  new command we chose \simpleinductive{}. In the package we want to support
-  some ``advanced'' features: First, we want that the package can cope with
-  specifications inside locales. For example it should be possible to declare
+  new command we chose \simpleinductive{}. The ``infrastructure'' already 
+  provides an ``advanced'' feature for this command. For example we will 
+  be able to declare the locale
 *}
 
 locale rel =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 
 text {*
-  and then define the transitive closure and the accessible part as follows:
+  and then define the transitive closure and the accessible part of this 
+  locale as follows:
 *}
 
-
 simple_inductive (in rel) 
   trcl' 
 where
@@ -31,68 +31,6 @@
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
 
-text {* 
-  Second, we want that the user can specify fixed parameters.
-  Remember in the previous section we stated that the user can give the 
-  specification for the transitive closure of a relation @{text R} as 
-*}
-
-simple_inductive
-  trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl\<iota>\<iota> R x x"
-| step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z"
-
-text {*
-  Note that there is no locale given in this specification---the parameter
-  @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
-  stays fixed throughout the specification. The problem with this way of
-  stating the specification for the transitive closure is that it derives the
-  following induction principle.
-
-  \begin{center}\small
-  \mprset{flushleft}
-  \mbox{\inferrule{
-             @{thm_style prem1  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem2  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
-             @{thm_style prem3  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
-            {@{thm_style concl  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}  
-  \end{center}
-
-  But this does not correspond to the induction principle we derived by hand, which
-  was
-  
-  \begin{center}\small
-  \mprset{flushleft}
-  \mbox{\inferrule{
-             @{thm_style prem1  trcl_induct[no_vars]}\\\\
-             @{thm_style prem2  trcl_induct[no_vars]}\\\\
-             @{thm_style prem3  trcl_induct[no_vars]}}
-            {@{thm_style concl  trcl_induct[no_vars]}}}  
-  \end{center}
-
-  The difference is that in the one derived by hand the relation @{term R} is not
-  a parameter of the proposition @{term P} to be proved and it is also not universally
-  qunatified in the second and third premise. The point is that the parameter @{term R}
-  stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''
-  argument of the transitive closure, but one that can be freely instantiated. 
-  In order to recognise such parameters, we have to extend the specification
-  to include a mechanism to state fixed parameters. The user should be able
-  to write 
-
-*}
-
-simple_inductive
-  trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  base: "trcl'' R x x"
-| step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"
-
-simple_inductive
-  accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
-
 text {*
   \begin{figure}[t]
   \begin{isabelle}
@@ -102,7 +40,7 @@
   \railalias{where}{\isacommand{where}}
   \railalias{for}{\isacommand{for}}
   \begin{rail}
-  simpleinductive target? fixes (for fixes)? \\
+  simpleinductive target?\\ fixes
   (where (thmdecl? prop + '|'))?
   ;
   \end{rail}
@@ -110,8 +48,7 @@
   \caption{A railroad diagram describing the syntax of \simpleinductive{}. 
   The \emph{target} indicates an optional locale; the \emph{fixes} are an 
   \isacommand{and}-separated list of names for the inductive predicates (they
-  can also contain typing- and syntax anotations); similarly the \emph{fixes} 
-  after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a 
+  can also contain typing- and syntax anotations); \emph{prop} stands for a 
   introduction rule with an optional theorem declaration (\emph{thmdecl}).
   \label{fig:railroad}}
   \end{figure}
@@ -121,9 +58,17 @@
   This leads directly to the railroad diagram shown in
   Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram
   more or less translates directly into the parser:
+*}
 
-  @{ML_chunk [display,gray] parser}
+ML %linenosgray{*val spec_parser = 
+     OuterParse.fixes -- 
+     Scan.optional 
+       (OuterParse.$$$ "where" |--
+          OuterParse.!!! 
+            (OuterParse.enum1 "|" 
+               (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
 
+text {*
   which we described in Section~\ref{sec:parsingspecs}. If we feed into the 
   parser the string (which corresponds to our definition of @{term even} and 
   @{term odd}):

--- a/ProgTutorial/Package/Ind_Prelims.thy	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Tue Mar 31 20:31:18 2009 +0100
@@ -5,37 +5,48 @@
 section{* Preliminaries *}
   
 text {*
-  The user will just give a specification of an inductive predicate and
+  The user will just give a specification of inductive predicate(s) and
   expects from the package to produce a convenient reasoning
   infrastructure. This infrastructure needs to be derived from the definition
-  that correspond to the specified predicate. This will roughly mean that the
-  package has three main parts, namely:
-
-
-  \begin{itemize}
-  \item parsing the specification and typing the parsed input,
-  \item making the definitions and deriving the reasoning infrastructure, and
-  \item storing the results in the theory. 
-  \end{itemize}
-
-  Before we start with explaining all parts, let us first give three examples
-  showing how to define inductive predicates by hand and then also how to
-  prove by hand important properties about them. From these examples, we will
+  that correspond to the specified predicate(s). Before we start with
+  explaining all parts of the package, let us first give four examples showing
+  how to define inductive predicates by hand and then also how to prove by
+  hand properties about them. See Figure \ref{fig:paperpreds} for their usual
+  ``pencil-and-paper'' definitions. From these examples, we will
   figure out a general method for defining inductive predicates.  The aim in
   this section is \emph{not} to write proofs that are as beautiful as
   possible, but as close as possible to the ML-code we will develop in later
   sections.
 
-
-  We first consider the transitive closure of a relation @{text R}. It is
-  an inductive predicate characterised by the two introduction rules:
-
+  \begin{figure}[t]
+  \begin{boxedminipage}{\textwidth}
   \begin{center}\small
   @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm}
   @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}
   \end{center}
+  \begin{center}\small
+  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
+  @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}
+  @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}
+  \end{center}
+  \begin{center}\small
+  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
+  \end{center}
+  \begin{center}\small
+  @{prop[mode=Rule] "a\<noteq>b \<Longrightarrow> fresh a (Var b)"}\hspace{5mm}
+  @{prop[mode=Rule] "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"}\\[2mm]
+  @{prop[mode=Axiom] "fresh a (Lam a t)"}\hspace{5mm}
+  @{prop[mode=Rule] "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}
+  \end{center}
+  \end{boxedminipage}
+  \caption{Examples of four ``Pencil-and-paper'' definitions of inductively defined
+  predicates. In formal reasoning with Isabelle, the user just wants to give such 
+  definitions and expects that the reasoning structure is derived automatically. 
+  For this definitional packages need to be implemented.\label{fig:paperpreds}}
+  \end{figure}
 
-  In Isabelle, the user will state for @{term trcl\<iota>} the specification:
+  We first consider the transitive closure of a relation @{text R}. The user will 
+  state for @{term trcl\<iota>} the specification:
 *}
 
 simple_inductive
@@ -45,7 +56,7 @@
 | step: "trcl\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota> R x z"
 
 text {*
-  As said above the package has to make an appropriate definition and provide
+  The package has to make an appropriate definition and provide
   lemmas to reason about the predicate @{term trcl\<iota>}. Since an inductively
   defined predicate is the least predicate closed under a collection of
   introduction rules, the predicate @{text "trcl R x y"} can be defined so
@@ -58,25 +69,25 @@
                   \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y"
 
 text {*
-  where we quantify over the predicate @{text P}. We have to use the
-  object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for
-  stating this definition (there is no other way for definitions in
-  HOL). However, the introduction rules and induction principles 
-  should use the meta-connectives since they simplify the
-  reasoning for the user.
+  We have to use the object implication @{text "\<longrightarrow>"} and object quantification
+  @{text "\<forall>"} for stating this definition (there is no other way for
+  definitions in HOL). However, the introduction rules and induction
+  principles associated with the transitive closure should use the meta-connectives, 
+  since they simplify the reasoning for the user.
+
 
   With this definition, the proof of the induction principle for @{term trcl}
   is almost immediate. It suffices to convert all the meta-level
   connectives in the lemma to object-level connectives using the
   proof method @{text atomize} (Line 4), expand the definition of @{term trcl}
   (Line 5 and 6), eliminate the universal quantifier contained in it (Line~7),
-  and then solve the goal by assumption (Line 8).
+  and then solve the goal by @{text assumption} (Line 8).
 
 *}
 
 lemma %linenos trcl_induct:
-  assumes "trcl R x y"
-  shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
+assumes "trcl R x y"
+shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
 apply(atomize (full))
 apply(cut_tac prems)
 apply(unfold trcl_def)
@@ -90,7 +101,7 @@
 *}
 
 lemma %linenos trcl_base: 
-  shows "trcl R x x"
+shows "trcl R x x"
 apply(unfold trcl_def)
 apply(rule allI impI)+
 apply(drule spec)
@@ -110,9 +121,10 @@
 (*<*)oops(*>*)
 
 text {*
-  The two assumptions correspond to the introduction rules. Thus, all we have
-  to do is to eliminate the universal quantifier in front of the first
-  assumption (Line 5), and then solve the goal by assumption (Line 6).
+  The two assumptions come from the definition of @{term trcl} and correspond
+  to the introduction rules. Thus, all we have to do is to eliminate the
+  universal quantifier in front of the first assumption (Line 5), and then
+  solve the goal by assumption (Line 6).
 *}
 
 text {*
@@ -123,7 +135,7 @@
 *}
 
 lemma trcl_step: 
-  shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
 apply (unfold trcl_def)
 apply (rule allI impI)+
 
@@ -147,8 +159,8 @@
   
 txt {*
   The assumptions @{text "p1"} and @{text "p2"} correspond to the premises of
-  the second introduction rule; the assumptions @{text "r1"} and @{text "r2"}
-  correspond to the introduction rules. We apply @{text "r2"} to the goal
+  the second introduction rule (unfolded); the assumptions @{text "r1"} and @{text "r2"}
+  come from the definition of @{term trcl} . We apply @{text "r2"} to the goal
   @{term "P x z"}. In order for the assumption to be applicable as a rule, we
   have to eliminate the universal quantifier and turn the object-level
   implications into meta-level ones. This can be accomplished using the @{text
@@ -183,7 +195,7 @@
 *}
 
 lemma trcl_step_blast: 
-  shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
+shows "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"
 apply(unfold trcl_def)
 apply(blast)
 done
@@ -195,20 +207,12 @@
   declare new intro- or simplification rules that can throw automatic tactics
   off course) and also it is very hard to debug proofs involving automatic
   tactics whenever something goes wrong. Therefore if possible, automatic 
-  tactics should be avoided or sufficiently constrained.
+  tactics should be avoided or be constrained sufficiently.
 
   The method of defining inductive predicates by impredicative quantification
   also generalises to mutually inductive predicates. The next example defines
-  the predicates @{text even} and @{text odd} characterised by the following
-  rules:
- 
-  \begin{center}\small
-  @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm}
-  @{prop[mode=Rule] "odd n \<Longrightarrow> even (Suc n)"} \hspace{5mm}
-  @{prop[mode=Rule] "even n \<Longrightarrow> odd (Suc n)"}
-  \end{center}
-  
-  The user will state for this inductive definition the specification:
+  the predicates @{text even} and @{text odd}. The user will state for this 
+  inductive definition the specification:
 *}
 
 simple_inductive
@@ -238,9 +242,8 @@
 *}
 
 lemma even_induct:
-  assumes "even n"
-  shows "P 0 \<Longrightarrow> 
-             (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+assumes "even n"
+shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
 apply(atomize (full))
 apply(cut_tac prems)
 apply(unfold even_def)
@@ -252,14 +255,14 @@
 text {*
   The only difference with the proof @{text "trcl_induct"} is that we have to
   instantiate here two universal quantifiers.  We omit the other induction
-  principle that has @{term "Q n"} as conclusion.  The proofs of the
-  introduction rules are also very similar to the ones in the @{text
-  "trcl"}-example. We only show the proof of the second introduction rule.
-
+  principle that has @{prop "even n"} as premise and @{term "Q n"} as conclusion.  
+  The proofs of the introduction rules are also very similar to the ones in 
+  the @{text "trcl"}-example. We only show the proof of the second introduction 
+  rule.
 *}
 
 lemma %linenos evenS: 
-  shows "odd m \<Longrightarrow> even (Suc m)"
+shows "odd m \<Longrightarrow> even (Suc m)"
 apply (unfold odd_def even_def)
 apply (rule allI impI)+
 proof -
@@ -277,6 +280,9 @@
 qed
 
 text {*
+  The interesting lines are 7 to 15. The assumptions fall into to categories:
+  @{text p1} corresponds to the premise of the introduction rule; @{text "r1"}
+  to @{text "r3"} come from the definition of @{text "even"}.
   In Line 13, we apply the assumption @{text "r2"} (since we prove the second
   introduction rule). In Lines 14 and 15 we apply assumption @{text "p1"} (if
   the second introduction rule had more premises we have to do that for all
@@ -284,41 +290,22 @@
   need to be instantiated and then also the implications need to be resolved
   with the other rules.
 
-
-  As a final example, we define the accessible part of a relation @{text R} characterised 
-  by the introduction rule
-  
-  \begin{center}\small
-  \mbox{\inferrule{@{term "\<And>y. R y x \<Longrightarrow> accpart R y"}}{@{term "accpart R x"}}}
-  \end{center}
-
-  whose premise involves a universal quantifier and an implication. The
+  As a final example, we define the accessible part of a relation @{text R}
+  (see Figure~\ref{fig:paperpreds}). There the premsise of the introduction 
+  rule involves a universal quantifier and an implication. The
   definition of @{text accpart} is:
 *}
 
 definition "accpart \<equiv> \<lambda>R x. \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x"
 
 text {*
-  The proof of the induction principle is again straightforward.
-*}
-
-lemma accpart_induct:
-  assumes "accpart R x"
-  shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
-apply(atomize (full))
-apply(cut_tac prems)
-apply(unfold accpart_def)
-apply(drule spec[where x=P])
-apply(assumption)
-done
-
-text {*
-  Proving the introduction rule is a little more complicated, because the quantifier
-  and the implication in the premise. The proof is as follows.
+  The proof of the induction principle is again straightforward and omitted.
+  Proving the introduction rule is a little more complicated, because the 
+  quantifier and the implication in the premise. The proof is as follows.
 *}
 
 lemma %linenos accpartI: 
-  shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
+shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply (unfold accpart_def)
 apply (rule allI impI)+
 proof -
@@ -338,9 +325,10 @@
 qed
 
 text {*
-  In Line 11, applying the assumption @{text "r1"} generates a goal state with
-  the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the 
-  proof above (Line 14). This local assumption is used to solve
+  There are now two subproofs. The assumptions fall again into two categories (Lines
+  7 to 9). In Line 11, applying the assumption @{text "r1"} generates a goal state 
+  with the new local assumption @{term "R y x"}, named @{text "r1_prem"} in the 
+  proof (Line 14). This local assumption is used to solve
   the goal @{term "P y"} with the help of assumption @{text "p1"}.
 
   The point of these examples is to get a feeling what the automatic proofs 

--- a/ProgTutorial/Parsing.thy	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Mar 31 20:31:18 2009 +0100
@@ -918,15 +918,16 @@
 
 ML{*let
   fun trace_top_lvl str = 
-     Toplevel.theory (fn thy => (tracing str; thy))
+     LocalTheory.theory (fn lthy => (tracing str; lthy))
 
   val trace_prop = OuterParse.prop >> trace_top_lvl
 
   val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
+  OuterSyntax.local_theory "foobar" "traces a proposition" kind trace_prop
 end *}
 
+
 text {*
   Now you can type
 

--- a/ProgTutorial/document/root.rao	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/document/root.rao	Tue Mar 31 20:31:18 2009 +0100
@@ -1,8 +1,8 @@
-% This file was generated by 'rail' from 'CookBook/generated/root.rai'
+% This file was generated by 'rail' from 'ProgTutorial/generated/root.rai'
 \rail@t {simpleinductive}
 \rail@t {where}
 \rail@t {for}
-\rail@i {1}{ simpleinductive target? fixes (for fixes)? \\ (where (thmdecl? prop + '|'))? ; }
+\rail@i {1}{ simpleinductive target?\\ fixes (where (thmdecl? prop + '|'))? ; }
 \rail@o {1}{
 \rail@begin{7}{}
 \rail@token{simpleinductive}[]
@@ -10,14 +10,9 @@
 \rail@nextbar{1}
 \rail@nont{target}[]
 \rail@endbar
+\rail@cr{3}
 \rail@nont{fixes}[]
 \rail@bar
-\rail@nextbar{1}
-\rail@token{for}[]
-\rail@nont{fixes}[]
-\rail@endbar
-\rail@cr{3}
-\rail@bar
 \rail@nextbar{4}
 \rail@token{where}[]
 \rail@plus

--- a/ProgTutorial/document/root.tex	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/document/root.tex	Tue Mar 31 20:31:18 2009 +0100
@@ -14,6 +14,7 @@
 \usepackage{framed}
 \usepackage{boxedminipage}
 \usepackage{mathpartir}
+\usepackage{flafter}
 \usepackage{pdfsetup}
 
 \urlstyle{rm}

Binary file progtutorial.pdf has changed