--- a/ProgTutorial/Parsing.thy	Mon May 17 17:27:21 2010 +0100
+++ b/ProgTutorial/Parsing.thy	Mon May 17 18:20:48 2010 +0100
@@ -41,8 +41,8 @@
   "Pure/General/scan.ML"}. The second part of the library consists of
   combinators for dealing with specific token types, which are defined in the
   structure @{ML_struct OuterParse} in the file @{ML_file
-  "Pure/Isar/outer_parse.ML"}. In addition specific parsers for packages are 
-  defined in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments 
+  "Pure/Isar/parse.ML"}. In addition specific parsers for packages are 
+  defined in @{ML_file "Pure/Isar/parse_spec.ML"}. Parsers for method arguments 
   are defined in @{ML_file "Pure/Isar/args.ML"}.
   \end{readmore}
 
@@ -480,7 +480,7 @@
 
   \begin{readmore}
   The parser functions for the theory syntax are contained in the structure
-  @{ML_struct OuterParse} defined in the file @{ML_file  "Pure/Isar/outer_parse.ML"}.
+  @{ML_struct OuterParse} defined in the file @{ML_file  "Pure/Isar/parse.ML"}.
   The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
   \end{readmore}
 
@@ -910,7 +910,7 @@
 text_raw {*
   \begin{exercise}
   Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
-  in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
+  in file @{ML_file "Pure/Isar/parse_spec.ML"}. This parser corresponds
   to the ``where-part'' of the introduction rules given above. Below
   we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our
   purposes. 

--- a/ProgTutorial/Solutions.thy	Mon May 17 17:27:21 2010 +0100
+++ b/ProgTutorial/Solutions.thy	Mon May 17 18:20:48 2010 +0100
@@ -254,7 +254,7 @@
     | _ => Conv.all_conv ctrm
 end
 
-val add_conv = More_Conv.bottom_conv add_simple_conv
+val add_conv = Conv.bottom_conv add_simple_conv
 
 fun add_tac ctxt = CONVERSION (add_conv ctxt)*}
 

--- a/ProgTutorial/Tactical.thy	Mon May 17 17:27:21 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Mon May 17 18:20:48 2010 +0100
@@ -2262,7 +2262,7 @@
   "True \<or> P \<equiv> True \<or> P"}
 
   Rewriting with more than one theorem can be done using the function 
-  @{ML_ind rewrs_conv in More_Conv} from the structure @{ML_struct More_Conv}.
+  @{ML_ind rewrs_conv in Conv} from the structure @{ML_struct Conv}.
   
 
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
@@ -2345,21 +2345,21 @@
 text {*
   Conversions that traverse terms, like @{ML true_conj1_conv} above, can be
   implemented more succinctly with the combinators @{ML_ind bottom_conv in
-  More_Conv} and @{ML_ind top_conv in More_Conv}. For example:
+  Conv} and @{ML_ind top_conv in Conv}. For example:
 *}
 
 ML{*fun true_conj1_conv ctxt =
 let
   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
 in
-  More_Conv.bottom_conv (K conv) ctxt
+  Conv.bottom_conv (K conv) ctxt
 end*}
 
 text {*
   If we regard terms as trees with variables and constants on the top, then 
-  @{ML bottom_conv in More_Conv} traverses first the the term and
+  @{ML bottom_conv in Conv} traverses first the the term and
   on the ``way down'' applies the conversion, whereas @{ML top_conv in
-  More_Conv} applies the conversion on the ``way up''. To see the difference, 
+  Conv} applies the conversion on the ``way up''. To see the difference, 
   assume the following two meta-equations
 *}
 
@@ -2378,9 +2378,9 @@
   @{ML_response_fake [display, gray]
   "let
   val ctxt = @{context}
-  val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc})
-  val conv_top = More_Conv.top_conv (K conv) ctxt
-  val conv_bot = More_Conv.bottom_conv (K conv) ctxt
+  val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
+  val conv_top = Conv.top_conv (K conv) ctxt
+  val conv_bot = Conv.bottom_conv (K conv) ctxt
   val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
 in
   (conv_top ctrm, conv_bot ctrm)
@@ -2400,13 +2400,13 @@
       Conv.arg_conv (true_conj1_conv ctxt) ctrm
   | _ => Conv.no_conv ctrm 
 
-val if_true1_conv = More_Conv.top_sweep_conv if_true1_simple_conv*}
+val if_true1_conv = Conv.top_sweep_conv if_true1_simple_conv*}
 
 text {*
   In the first function we only treat the top-most redex and also only the
   success case. As default we return @{ML no_conv in Conv}.  To apply this
   ``simple'' conversion inside a term, we use in the last line the combinator @{ML_ind
-  top_sweep_conv in More_Conv}, which traverses the term starting from the
+  top_sweep_conv in Conv}, which traverses the term starting from the
   root and applies it to all the redexes on the way, but stops in each branch as
   soon as it found one redex. Here is an example for this conversion:
 
@@ -2496,7 +2496,7 @@
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
   the conclusion according to @{ML true_conj1_conv}. If we only have one
   conversion that should be uniformly applied to the whole goal state, we
-  can simplify @{ML true1_tac} using @{ML_ind top_conv in More_Conv}.
+  can simplify @{ML true1_tac} using @{ML_ind top_conv in Conv}.
 
   Conversions are also be helpful for constructing meta-equality theorems.
   Such theorems are often definitions. As an example consider the following
@@ -2592,7 +2592,7 @@
   \end{exercise}
 
   \begin{readmore}
-  See @{ML_file "Pure/conv.ML"} and  @{ML_file "Tools/more_conv.ML"}
+  See @{ML_file "Pure/conv.ML"}
   for more information about conversion combinators. 
   Some basic conversions are defined in  @{ML_file "Pure/thm.ML"},
   @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.

Binary file progtutorial.pdf has changed