--- a/ProgTutorial/FirstSteps.thy	Fri Jun 05 04:17:28 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Tue Jun 23 04:05:01 2009 +0200
@@ -2136,6 +2136,6 @@
 
 section {* Misc (TBD) *}
 
-ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
+ML {*Datatype.get_datatype @{theory} "List.list"*}
 
 end

--- a/ProgTutorial/Package/Ind_Extensions.thy	Fri Jun 05 04:17:28 2009 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue Jun 23 04:05:01 2009 +0200
@@ -184,7 +184,7 @@
   The standard inductive package is based on least fix-points. It allows more 
   general introduction rules that can include any monotone operators and also
   provides a richer reasoning infrastructure. The code of this package can be found in 
-  @{ML_file "HOL/Tools/inductive_package.ML"}.
+  @{ML_file "HOL/Tools/inductive.ML"}.
   \end{readmore}
 *}
 
@@ -192,7 +192,7 @@
 
 text {* Type declarations *}
 
-ML{*TypedefPackage.add_typedef false NONE (@{binding test},[],NoSyn)
+ML{*Typedef.add_typedef false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
 

--- a/ProgTutorial/Parsing.thy	Fri Jun 05 04:17:28 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Tue Jun 23 04:05:01 2009 +0200
@@ -75,17 +75,17 @@
   In the examples above we use the function @{ML Symbol.explode}, instead of the 
   more standard library function @{ML explode}, for obtaining an input list for 
   the parser. The reason is that @{ML Symbol.explode} is aware of character sequences,
-  for example @{text "\\<foo>"}, that have a special meaning in Isabelle. To see
+  for example @{text "\<foo>"}, that have a special meaning in Isabelle. To see
   the difference consider
 
 @{ML_response_fake [display,gray]
 "let 
-  val input = \"\\<foo> bar\"
+  val input = \"\<foo> bar\"
 in
   (explode input, Symbol.explode input)
 end"
 "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
- [\"\\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
+ [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
 
   Slightly more general than the parser @{ML "$$"} is the function 
   @{ML [index] one in Scan}, in that it takes a predicate as argument and 

--- a/ProgTutorial/antiquote_setup.ML	Fri Jun 05 04:17:28 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue Jun 23 04:05:01 2009 +0200
@@ -20,7 +20,7 @@
 
 fun ml_pat (lhs, pat) =
   let 
-     val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
+     val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
   in "val " ^ pat' ^ " = " ^ lhs end;
 
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";

--- a/ProgTutorial/output_tutorial.ML	Fri Jun 05 04:17:28 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Tue Jun 23 04:05:01 2009 +0200
@@ -51,7 +51,7 @@
     | "}" => "\\}"
     | "$" => "\\isachardollar"
     | "!" => "\\isacharbang"
-    | "\\<dash>" => "-"
+    | "\<dash>" => "-"
     | c => c);
 
 fun get_word str =

Binary file progtutorial.pdf has changed