--- a/ProgTutorial/Essential.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/Essential.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -127,7 +127,7 @@
 
   When constructing terms, you are usually concerned with free
   variables (as mentioned earlier, you cannot construct schematic
-  variables using the built in antiquotation \mbox{@{text "@{term
+  variables using the built-in antiquotation \mbox{@{text "@{term
   \<dots>}"}}). If you deal with theorems, you have to, however, observe the
   distinction. The reason is that only schematic variables can be
   instantiated with terms when a theorem is applied. A similar
@@ -148,7 +148,7 @@
   "@{term \"x x\"}"
   "Type unification failed: Occurs check!"}
 
-  raises a typing error, while it perfectly ok to construct the term
+  raises a typing error, while it is perfectly ok to construct the term
   with the raw ML-constructors:
 
   @{ML_response_fake [display,gray] 
@@ -276,7 +276,7 @@
   that it is defined in the theory @{text "List"}. However, one has to be 
   careful with names of types, because even if
   @{text "fun"} is defined in the theory @{text "HOL"}, it is  
-  still represented by their simple name.
+  still represented by its simple name.
 
    @{ML_response [display,gray]
   "@{typ \"bool \<Rightarrow> nat\"}"
@@ -379,7 +379,7 @@
 end"
   "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
-  In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
+  In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML "Bound 0"}), 
   and an abstraction, where it also records the type of the abstracted
   variable and for printing purposes also its name.  Note that because of the
   typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
@@ -792,7 +792,7 @@
   The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
   environment, which is needed for starting the unification without any
   (pre)instantiations. The @{text 0} is an integer index that will be explained
-  below. In case of failure, @{ML typ_unify in Sign} will throw the exception
+  below. In case of failure, @{ML typ_unify in Sign} will raise the exception
   @{text TUNIFY}.  We can print out the resulting type environment bound to 
   @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
   structure @{ML_struct Vartab}.
@@ -1123,7 +1123,7 @@
 
   As mentioned before, unrestricted higher-order unification, respectively
   unrestricted higher-order matching, is in general undecidable and might also
-  not posses a single most general solution. Therefore Isabelle implements the
+  not possess a single most general solution. Therefore Isabelle implements the
   unification function @{ML_ind unifiers in Unify} so that it returns a lazy
   list of potentially infinite unifiers.  An example is as follows
 *}
@@ -1200,7 +1200,7 @@
   problem can be solved by first-order matching.
 
   Higher-order matching might be necessary for instantiating a theorem
-  appropriately. More on this will be given in Sections~\ref{sec:theorems}. 
+  appropriately. More on this will be given in Section~\ref{sec:theorems}. 
   Here we only have a look at a simple case, namely the theorem 
   @{thm [source] spec}:
 
@@ -1212,7 +1212,7 @@
   as an introduction rule. Applying it directly can lead to unexpected
   behaviour since the unification has more than one solution. One way round
   this problem is to instantiate the schematic variables @{text "?P"} and
-  @{text "?x"}.  instantiation function for theorems is 
+  @{text "?x"}.  Instantiation function for theorems is 
   @{ML_ind instantiate_normalize in Drule} from the structure 
   @{ML_struct Drule}. One problem, however, is
   that this function expects the instantiations as lists of @{ML_type ctyp}
@@ -1309,10 +1309,10 @@
   Overloading a constant means specifying its value on a type based on
   a well-founded reduction towards other values of constants on types.
   When instantiating type classes
-  (i.e. proving arities) you are specifying overloading via primitive recursion.
+  (i.e.\ proving arities) you are specifying overloading via primitive recursion.
 
   Sorts are finite intersections of type classes and are implemented as lists
-  of type class names. The empty intersection, i.e. the empty list, is therefore
+  of type class names. The empty intersection, i.e.\ the empty list, is therefore
   inhabited by all types and is called the topsort.
 
   Free and schematic type variables are always annotated with sorts, thereby restricting
@@ -1348,7 +1348,7 @@
 section {* Type-Checking\label{sec:typechecking} *}
 
 text {* 
-  Remember Isabelle follows the Church-style typing for terms, i.e., a term contains 
+  Remember Isabelle follows the Church-style typing for terms, i.e.\ a term contains 
   enough typing information (constants, free variables and abstractions all have typing 
   information) so that it is always clear what the type of a term is. 
   Given a well-typed term, the function @{ML_ind type_of in Term} returns the 

--- a/ProgTutorial/First_Steps.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/First_Steps.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -105,7 +105,7 @@
 
   @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
 
-  However, @{text "@{makes_tring}"} only works if the type of what
+  However, @{text "@{make_string}"} only works if the type of what
   is converted is monomorphic and not a function. 
 
   You can print out error messages with the function @{ML_ind error in Library}; 
@@ -120,12 +120,12 @@
   be displayed by the infrastructure indicating that it is an error by
   painting the output red. Note that this exception is meant 
   for ``user-level'' error messages seen by the ``end-user''. 
-  For messages where you want to indicate a genuine program error, then
+  For messages where you want to indicate a genuine program error
   use the exception @{text Fail}. 
 
-  Most often you want to inspect data of Isabelle's basic data structures,
+  Most often you want to inspect contents of Isabelle's basic data structures,
   namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
-  and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
+  and @{ML_type thm}. Isabelle provides elaborate pretty-printing functions,
   which we will explain in more detail in Section \ref{sec:pretty}. For now
   we just use the functions @{ML_ind writeln in Pretty}  from the structure
   @{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
@@ -136,7 +136,7 @@
 val pwriteln = Pretty.writeln*}
 
 text {*
-  They can now be used as follows
+  They can be used as follows
 
   @{ML_response_fake [display,gray]
   "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
@@ -151,8 +151,8 @@
   Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
 
 text {*
-  You can also print out terms together with their typing information.
-  For this you need to set the configuration value  
+  To print out terms together with their typing information,
+  set the configuration value
   @{ML_ind show_types in Syntax} to @{ML true}.
 *}
 
@@ -165,7 +165,7 @@
   "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
   "(1::nat, x::'a)"}
 
-  where @{text 1} and @{text x} are displayed with their inferred type.
+  where @{text 1} and @{text x} are displayed with their inferred types.
   Other configuration values that influence
   printing of terms include 
 
@@ -200,8 +200,8 @@
 
 text {*
   Theorems include schematic variables, such as @{text "?P"}, 
-  @{text "?Q"} and so on. They are needed in Isabelle in order to able to
-  instantiate theorems when they are applied. For example the theorem 
+  @{text "?Q"} and so on. They are instantiated by Isabelle when a theorem is applied.
+  For example, the theorem 
   @{thm [source] conjI} shown below can be used for any (typable) 
   instantiation of @{text "?P"} and @{text "?Q"}. 
 
@@ -209,7 +209,7 @@
   "pwriteln (pretty_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
-  However, in order to improve the readability when printing theorems, we
+  However, to improve the readability when printing theorems, we
   can switch off the question marks as follows:
 *}
 
@@ -367,9 +367,9 @@
 in y4 end*}
 
 text {* 
-  Another reason why the let-bindings in the code above are better to be
-  avoided: it is more than easy to get the intermediate values wrong, not to 
-  mention the nightmares the maintenance of this code causes!
+  Another reasons to avoid the let-bindings in the code above:
+  it is easy to get the intermediate values wrong and
+  the resulting code is difficult to maintain.
 
   In Isabelle a ``real world'' example for a function written in 
   the waterfall fashion might be the following code:
@@ -384,9 +384,9 @@
       |> curry list_comb f *}
 
 text {*
-  This function takes a term and a context as argument. If the term is of function
+  This function takes a term and a context as arguments. If the term is of function
   type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
-  applied to it. For example below three variables are applied to the term 
+  applied to it. For example, below three variables are applied to the term 
   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 
   @{ML_response_fake [display,gray]
@@ -463,7 +463,7 @@
 text {*
   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 
   @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory}; 
-  its purpose is to store a theorem under a name. 
+  it stores a theorem under a name. 
   In lines 5 to 6 we call this function to give alternative names for the three
   theorems. The point of @{ML "#>"} is that you can sequence such function calls. 
 
@@ -770,7 +770,7 @@
 
   Another important antiquotation is @{text "@{context}"}. (What the
   difference between a theory and a context is will be described in Chapter
-  \ref{chp:advanced}.) A context is for example needed in order to use the
+  \ref{chp:advanced}.) A context is for example needed to use the
   function @{ML print_abbrevs in Proof_Context} that list of all currently
   defined abbreviations. For example
 
@@ -853,8 +853,8 @@
 
   It is also possible to define your own antiquotations. But you should
   exercise care when introducing new ones, as they can also make your code
-  also difficult to read. In the next chapter we describe how to construct
-  terms with the (build in) antiquotation @{text "@{term \<dots>}"}.  A restriction
+  difficult to read. In the next chapter we describe how to construct
+  terms with the (built-in) antiquotation @{text "@{term \<dots>}"}.  A restriction
   of this antiquotation is that it does not allow you to use schematic
   variables in terms. If you want to have an antiquotation that does not have
   this restriction, you can implement your own using the function @{ML_ind
@@ -918,8 +918,8 @@
 setup %gray {* type_pat_setup *}
 
 text {* 
-However, a word of warning is in order: Introducing new antiquotations should be done only after
-careful deliberations. They can potentially make your code harder to read, than making it easier.
+However, a word of warning is in order: new antiquotations should be introduced only after
+careful deliberations. They can potentially make your code harder, rather than easier, to read.
 
   \begin{readmore}
   The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
@@ -1010,7 +1010,7 @@
   are only relevant to the proof at hand. Therefore such data needs to be 
   maintained inside a proof context, which represents ``local'' data.
   You can think of a theory as the ``longterm memory'' of Isabelle (nothing will
-  be deleted from it), and a proof-context as a ``shortterm memory'' (it dynamically
+  be deleted from it), and a proof-context as a ``shortterm memory'' (it
   changes according to what is needed at the time).
 
   For theories and proof contexts there are, respectively, the functors 
@@ -1042,7 +1042,7 @@
   defaults.\footnote{\bf FIXME: Say more about the
   assumptions of these operations.} The result structure @{ML_text Data}
   contains functions for accessing the table (@{ML Data.get}) and for updating
-  it (@{ML Data.map}). There is also the functions @{ML Data.put}, which however is 
+  it (@{ML Data.map}). There is also the function @{ML Data.put}, but it is 
   not relevant here. Below we define two
   auxiliary functions, which help us with accessing the table.
 *}
@@ -1064,7 +1064,7 @@
 text {*
   The use of the command \isacommand{setup} makes sure the table in the 
   \emph{current} theory is updated (this is explained further in 
-  section~\ref{sec:theories}). The lookup can now be performed as follows.
+  Section~\ref{sec:theories}). The lookup can now be performed as follows.
 
   @{ML_response_fake [display, gray]
 "lookup @{theory} \"conj\""

--- a/ProgTutorial/Parsing.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/Parsing.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -79,11 +79,11 @@
   There are three exceptions that are raised by the parsing combinators:
 
   \begin{itemize}
-  \item @{text "FAIL"} is used to indicate that alternative routes of parsing 
+  \item @{text "FAIL"} indicates that alternative routes of parsing 
   might be explored. 
   \item @{text "MORE"} indicates that there is not enough input for the parser. For example 
   in @{text "($$ \"h\") []"}.
-  \item @{text "ABORT"} is the exception that is raised when a dead end is reached. 
+  \item @{text "ABORT"} indicates that a dead end is reached. 
   It is used for example in the function @{ML "!!"} (see below).
   \end{itemize}
 
@@ -142,7 +142,7 @@
 
   Parsers that explore alternatives can be constructed using the function 
   @{ML_ind  "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
-  result of @{text "p"}, in case it succeeds, otherwise it returns the
+  result of @{text "p"}, in case it succeeds; otherwise it returns the
   result of @{text "q"}. For example:
 
 
@@ -173,7 +173,7 @@
   "((\"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 
+  @{text "p"}, in case it succeeds; otherwise it returns 
   the default value @{text "x"}. For example:
 
 @{ML_response [display,gray]
@@ -220,7 +220,7 @@
   hence the alternative parser @{text r} will be tried. However, in many
   circumstances this will be the wrong parser for the input ``@{text "p"}-followed-by-something''
   and therefore will also fail. The error message is then caused by the failure
-  of @{text r}, not by the absence of @{text q} in the input. This kind of
+  of @{text r}, not by the absence of @{text q} in the input. Such
   situation can be avoided when using the function @{ML "!!"}.  This function
   aborts the whole process of parsing in case of a failure and prints an error
   message. For example if you invoke the parser
@@ -280,7 +280,7 @@
   yields the expected parsing. 
 
   The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as 
-  often as it succeeds. For example:
+  long as it succeeds. For example:
   
   @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")" 
                 "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
@@ -970,7 +970,7 @@
   ...
   \end{graybox}
 
-  whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the
+  where @{ML_ind "thy_decl" in Keyword} indicates the kind of the
   command.  Another possible kind is @{text "thy_goal"}, or you can
   also omit the kind entirely, in which case you declare a keyword
   (something that is part of a command).
@@ -1190,7 +1190,7 @@
 text {*
   In order to use a new command in Emacs and Proof-General, you need a keyword
   file that can be loaded by ProofGeneral. To keep things simple we take as
-  running example the command \isacommand{foobar} from the previous section. 
+  a running example the command \isacommand{foobar} from the previous section. 
 
   A keyword file can be generated with the command-line:
 
@@ -1230,6 +1230,7 @@
   \end{figure}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+
   For our purposes it is sufficient to use the log files of the theories
   @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
   the log file for the theory @{text "Command.thy"}, which contains the new
@@ -1238,7 +1239,7 @@
   
   @{text Pure} and @{text HOL} are usually compiled during the installation of
   Isabelle. So log files for them should be already available. If not, then
-  they can be conveniently compiled with the help of the build-script from the Isabelle
+  they can be easily compiled with the build-script from the Isabelle
   distribution.
 
   @{text [display] 
@@ -1251,26 +1252,24 @@
 
   For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory 
   with:
-
-  @{text [display] "$ isabelle mkdir FoobarCommand"}
+ 
+  @{text [display] "$ isabelle mkroot -d FoobarCommand"}
 
   This generates a directory containing the files: 
-
+  
   @{text [display] 
-"./IsaMakefile
-./FoobarCommand/ROOT.ML
+"./FoobarCommand/ROOT
 ./FoobarCommand/document
 ./FoobarCommand/document/root.tex"}
-
-
+ 
   You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
   and add the line 
 
   @{text [display] "no_document use_thy \"Command\";"} 
   
-  to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing:
+  to the file @{text "./FoobarCommand/ROOT"}. You can now compile the theory by just typing:
 
-  @{text [display] "$ isabelle make"}
+  @{text [display] "$ isabelle build"}
 
   If the compilation succeeds, you have finally created all the necessary log files. 
   They are stored in the directory 
@@ -1469,7 +1468,7 @@
 text {*
   (FIXME: maybe move to after the tactic section)
 
-  Methods are central to Isabelle. They are the ones you use for example
+  Methods are central to Isabelle. You use them, for example,
   in \isacommand{apply}. To print out all currently known methods you can use the 
   Isabelle command:
 

--- a/ProgTutorial/Tactical.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -18,13 +18,13 @@
   Donald E.~Knuth, from an interview in Dr.~Dobb's Journal, 1996.
   \end{flushright}
 
-  One of the main reason for descending to the ML-level of Isabelle is to be
-  able to implement automatic proof procedures. Such proof procedures can
+  One of the main reason for descending to the ML-level of Isabelle is to
+  implement automatic proof procedures. Such proof procedures can
   considerably lessen the burden of manual reasoning. They are centred around
   the idea of refining a goal state using tactics. This is similar to the
   \isacommand{apply}-style reasoning at the user-level, where goals are
   modified in a sequence of proof steps until all of them are discharged.
-  In this chapter we will explain simple tactics and how to combine them using
+  In this chapter we explain how to implement simple tactics and how to combine them using
   tactic combinators. We also describe the simplifier, simprocs and conversions.
 *}
 
@@ -113,7 +113,7 @@
 text {*
   By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the 
   user-level of Isabelle the tactic @{ML foo_tac} or 
-  any other function that returns a tactic. There are some goal transformation
+  any other function that returns a tactic. There are some goal transformations
   that are performed by @{text "tactic"}. They can be avoided by using 
   @{text "raw_tactic"} instead.
 
@@ -138,7 +138,7 @@
   one such combinator---a ``primed'' version exists.)  With @{ML foo_tac'} you
   can give the number for the subgoal explicitly when the tactic is called. So
   in the next proof you can first discharge the second subgoal, and
-  subsequently the first.
+  then the first.
 *}
 
 lemma 
@@ -152,8 +152,8 @@
   This kind of addressing is more difficult to achieve when the goal is 
   hard-coded inside the tactic. 
 
-  The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for analysing
-  goals being only of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
+  The tactics @{ML foo_tac} and @{ML foo_tac'} are specific
+  to goals of the form @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. If the goal is not of
   this form, then these tactics return the error message:\footnote{To be
   precise, tactics do not produce this error message; the message originates from the
   \isacommand{apply} wrapper that calls the tactic.}
@@ -173,8 +173,8 @@
 
 text {*
   By convention, if a tactic fails, then it should return the empty sequence. 
-  Therefore, if you write your own tactics, they  should not raise exceptions 
-  willy-nilly; only in very grave failure situations should a tactic raise the 
+  Therefore, your own tactics should not raise exceptions 
+  willy-nilly; only in very grave failure situations should a tactic raise the
   exception @{text THM}.
 
   The simplest tactics are @{ML_ind no_tac in Tactical} and 

--- a/ProgTutorial/document/build	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/document/build	Wed Oct 15 23:12:54 2014 +0100
@@ -26,4 +26,4 @@
 #+"$ISABELLE_TOOL" latex -o "$FORMAT"
 #+"$ISABELLE_TOOL" latex -o "$FORMAT"
 #$(ISABELLE_TOOL) document -o pdf  ProgTutorial/generated
-#	makeindex -o ProgTutorial/generated/root.stu ProgTutorial/generated/root.str 
\ No newline at end of file
+#	makeindex -o ProgTutorial/generated/root.stu ProgTutorial/generated/root.str 

--- a/ProgTutorial/document/mathpartir.sty	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/document/mathpartir.sty	Wed Oct 15 23:12:54 2014 +0100
@@ -3,7 +3,7 @@
 %  Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
 %
 %  Author         : Didier Remy 
-%  Version        : 1.2.0
+%  Version        : 1.2.1
 %  Bug Reports    : to author
 %  Web Site       : http://pauillac.inria.fr/~remy/latex/
 % 
@@ -255,19 +255,26 @@
 
 %% A generic solution to arrow
 
+\def \mpr@@fractionaboveskip {0ex}
+\def \mpr@@fractionbelowskip {0.22ex}
+
 \def \mpr@make@fraction #1#2#3#4#5{\hbox {%
      \def \mpr@tail{#1}%
      \def \mpr@body{#2}%
      \def \mpr@head{#3}%
      \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
      \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
-     \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
-     \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
-     \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
-     \setbox0=\hbox {$\box1 \@@atop \box2$}%
+     \dimen0\ht3\advance\dimen0 by \dp3\relax
+     \dimen0 0.5\dimen0\relax
+     \advance \dimen0 by \mpr@@fractionaboveskip
+     \setbox1=\hbox {\raise \dimen0 \box1}\relax
+     \dimen0 -\dimen0\advance \dimen0 \mpr@@fractionaboveskip\dimen0 -\dimen0
+     \advance \dimen0 by \mpr@@fractionbelowskip
+     \setbox2=\hbox {\lower \dimen0 \box2}\relax
+     \setbox0=\hbox {$\displaystyle {\box1 \atop \box2}$}%
      \dimen0=\wd0\box0
      \box0 \hskip -\dimen0\relax
-     \hbox to \dimen0 {$%
+     \hbox to \dimen0 {$%\color{blue}
        \mathrel{\mpr@tail}\joinrel
        \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
      $}}}
@@ -354,6 +361,7 @@
 \def \mprset #1{\setkeys{mprset}{#1}}
 \define@key {mprset}{andskip}[]{\mpr@andskip=#1}
 \define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{lessskip}[]{\lineskip=0.5\lineskip}
 \define@key {mprset}{flushleft}[]{\mpr@centerfalse}
 \define@key {mprset}{center}[]{\mpr@centertrue}
 \define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
@@ -361,6 +369,8 @@
 \define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
 \define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
 \define@key {mprset}{sep}{\def\mpr@sep{#1}}
+\define@key {mprset}{fractionaboveskip}{\def\mpr@@fractionaboveskip{#1}}
+\define@key {mprset}{fractionbelowskip}{\def\mpr@@fractionbelowskip{#1}}
 
 \newbox \mpr@right
 \define@key {mpr}{flushleft}[]{\mpr@centerfalse}

Binary file progtutorial.pdf has changed