--- a/ProgTutorial/FirstSteps.thy	Tue Jul 14 16:34:24 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Jul 20 16:52:59 2009 +0200
@@ -1305,8 +1305,35 @@
 
   (FIXME: how to add case-names to goal states - maybe in the 
   next section)
+
+  (FIXME: example for how to add theorem styles)
 *}
 
+ML {*
+fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) =
+      strip_assums_all ((a, T)::params, t)
+  | strip_assums_all (params, B) = (params, B)
+
+fun style_parm_premise i ctxt t =
+  let val prems = Logic.strip_imp_prems t in
+    if i <= length prems
+    then let val (params,t) = strip_assums_all([], nth prems (i - 1))
+         in subst_bounds(map Free params, t) end
+    else error ("Not enough premises for prem" ^ string_of_int i ^
+      " in propositon: " ^ Syntax.string_of_term ctxt t)
+  end;
+*}
+
+ML {*
+strip_assums_all ([], @{term "\<And>x y. A x y"})
+*}
+
+setup {*
+  TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
+  TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
+*}
+
+
 section {* Setups (TBD) *}
 
 text {*
@@ -1675,11 +1702,11 @@
   properly treats ``data slots''!
 
   Since storing theorems in a list is such a common task, there is the special
-  functor @{text NamedThmsFun}, which does most of the work for you. To obtain
+  functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain
   a named theorem lists, you just declare
 *}
 
-ML{*structure FooRules = NamedThmsFun 
+ML{*structure FooRules = Named_Thms
  (val name = "foo" 
   val description = "Rules for foo") *}
 

--- a/ProgTutorial/Intro.thy	Tue Jul 14 16:34:24 2009 +0200
+++ b/ProgTutorial/Intro.thy	Mon Jul 20 16:52:59 2009 +0200
@@ -149,7 +149,7 @@
   If you managed to do this, then the problem of the moving target goes 
   away, because when checking in code, developers are strongly urged to 
   test against Isabelle's code base. If your project is part of that code base, 
-  then code maintenance is done by others. Unfortunately, this might not
+  then maintenance is done by others. Unfortunately, this might not
   be a helpful advice for all types of projects. A lower threshold for inclusion has the 
   Archive of Formalised Proofs, short AFP.\footnote{\url{http://afp.sourceforge.net/}}
   This archive has been created mainly for formalisations that are

Binary file progtutorial.pdf has changed