# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256654601 -3600
# Node ID 8ba963a3e039384b2ae8c9967b88053d1c8815ba
# Parent  bdd411caf5ebf7918fce4c6587ee9a28f61b59c0
tuned

diff -r bdd411caf5eb -r 8ba963a3e039 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -674,8 +674,9 @@
 *}
 
 text {*
-  In this example we obtain three terms whose variables @{text m} and @{text
-  n} are of type @{typ "nat"}. If you have only a single term, then @{ML
+  In this example we obtain three terms (using @{ML_ind parse_term in Syntax}) whose 
+  variables @{text m} and @{text n} are of type @{typ "nat"}. If you have only 
+  a single term, then @{ML
   check_terms in Syntax} needs plumbing. This can be done with the function
   @{ML singleton}.\footnote{There is already a function @{ML check_term in
   Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
diff -r bdd411caf5eb -r 8ba963a3e039 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/General.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -1365,7 +1365,8 @@
 
 text {*
   This gives a function from @{ML_type "theory -> theory"}, which
-  can be used for example with \isacommand{setup}.
+  can be used for example with \isacommand{setup} or with
+  @{ML "Context.>> o Context.map_theory"}.
 
   As an example of a slightly more complicated theorem attribute, we implement 
   our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
@@ -1545,11 +1546,15 @@
   @{ML_type local_theory} is identical to the type of \emph{proof contexts}
   @{ML_type "Proof.context"}, although not every proof context constitutes a
   valid local theory.
+
+  @{ML "Context.>> o Context.map_theory"}
 *}
 
 section {* Setups (TBD) *}
 
 text {*
+  @{ML Sign.declare_const}
+
   In the previous section we used \isacommand{setup} in order to make
   a theorem attribute known to Isabelle. What happens behind the scenes
   is that \isacommand{setup} expects a function of type 
diff -r bdd411caf5eb -r 8ba963a3e039 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -691,6 +691,11 @@
   in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
   \end{readmore}
   
+  FIXME:
+  @{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax}
+  @{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax}
+  
+
 *}
 
 section {* Parsing Specifications\label{sec:parsingspecs} *}
diff -r bdd411caf5eb -r 8ba963a3e039 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Oct 26 00:00:26 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Oct 27 15:43:21 2009 +0100
@@ -1592,9 +1592,6 @@
 
   (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
 
-  (FIXME: @{ML ObjectLogic.full_atomize_tac}, 
-  @{ML ObjectLogic.rulify_tac})
-
   (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 
   (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
diff -r bdd411caf5eb -r 8ba963a3e039 progtutorial.pdf
Binary file progtutorial.pdf has changed