--- a/ProgTutorial/Package/Ind_Code.thy	Tue Mar 31 15:53:12 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Tue Mar 31 16:50:13 2009 +0100
@@ -1065,7 +1065,7 @@
                  OuterKeyword.thy_decl specification*}
 
 
-section {* Extensions *}
+section {* Extensions (TBD) *}
 
 text {*
   Things to include at the end:

--- a/ProgTutorial/Package/Ind_Intro.thy	Tue Mar 31 15:53:12 2009 +0100
+++ b/ProgTutorial/Package/Ind_Intro.thy	Tue Mar 31 16:50:13 2009 +0100
@@ -2,7 +2,7 @@
 imports Main 
 begin
 
-chapter {* How to Write a Definitional Package\label{chp:package} (TBD) *}
+chapter {* How to Write a Definitional Package\label{chp:package} *}
 
 text {*
   \begin{flushright}

--- a/ProgTutorial/Tactical.thy	Tue Mar 31 15:53:12 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Mar 31 16:50:13 2009 +0100
@@ -2107,15 +2107,12 @@
   }
 oops
 
-ML {* fun prop ctxt s =
-  Thm.cterm_of (ProofContext.theory_of ctxt) (Syntax.read_prop ctxt s) *}
-
 ML {* 
   val ctxt0 = @{context};
   val ctxt = ctxt0;
   val (_, ctxt) = Variable.add_fixes ["A", "B", "C"] ctxt;
-  val ([r], ctxt) = Assumption.add_assumes [prop ctxt "A & B \<Longrightarrow> C"] ctxt;
-  val (this, ctxt) = Assumption.add_assumes [prop ctxt "A", prop ctxt "B"] ctxt;
+  val ([r], ctxt) = Assumption.add_assumes [@{cprop "A & B \<Longrightarrow> C"}] ctxt
+  val (this, ctxt) = Assumption.add_assumes [@{cprop "A"}, @{cprop "B"}] ctxt;
   val this = [@{thm conjI} OF this]; 
   val this = r OF this;
   val this = Assumption.export false ctxt ctxt0 this 

Binary file progtutorial.pdf has changed