# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1248101579 -7200
# Node ID c354e45d80d2b97382198d7bedc5b320331bc013
# Parent  311830b43f8f6913b062419eb42e336bec25333b
small changes for latest changes in Isabelle

diff -r 311830b43f8f -r c354e45d80d2 ProgTutorial/FirstSteps.thy
--- 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") *}
 
diff -r 311830b43f8f -r c354e45d80d2 ProgTutorial/Intro.thy
--- 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
diff -r 311830b43f8f -r c354e45d80d2 progtutorial.pdf
Binary file progtutorial.pdf has changed