# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1320398990 0
# Node ID 490fe9483c0dadf97a51d9fb6a2f33969d708780
# Parent  69b5ba7518b93fa2d0cd9cb3db0c11c71a12cb07
more material

diff -r 69b5ba7518b9 -r 490fe9483c0d ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Thu Nov 03 17:53:36 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Fri Nov 04 09:29:50 2011 +0000
@@ -73,26 +73,26 @@
 section {* Setups (TBD) *}
 
 text {*
-  @{ML Sign.declare_const}
+  In the previous section we used \isacommand{setup}, for example, in
+  order to make a theorem attribute known to Isabelle. What happens
+  behind the scenes is that \isacommand{setup} expects a function of
+  type @{ML_type "theory -> theory"}: the input theory is the current
+  theory and the output the theory where the theory attribute has been
+  stored.
 
-  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 
-  @{ML_type "theory -> theory"}: the input theory is the current theory and the 
-  output the theory where the theory attribute has been stored.
-  
-  This is a fundamental principle in Isabelle. A similar situation occurs 
-  for example with declaring constants. The function that declares a 
-  constant on the ML-level is @{ML_ind  add_consts_i in Sign}. 
-  If you write\footnote{Recall that ML-code  needs to be 
+  This is a fundamental principle in Isabelle. A similar situation arises
+  with declaring constants. The function that declares a 
+  constant on the ML-level is @{ML_ind  declare_const in Sign}. 
+  However, if you simply write\footnote{Recall that ML-code  needs to be 
   enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} 
 *}  
 
-ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
+ML{*Sign.declare_const @{context} 
+  ((@{binding "BAR"}, @{typ "nat"}), NoSyn) @{theory} *}
 
 text {*
-  for declaring the constant @{text "BAR"} with type @{typ nat} and 
-  run the code, then you indeed obtain a theory as result. But if you 
+  with the intention of declaring the constant @{text "BAR"} with type @{typ nat} 
+  and  run the code, then indeed you obtain a theory as result. But if you 
   query the constant on the Isabelle level using the command \isacommand{term}
 
   \begin{isabelle}
@@ -100,13 +100,15 @@
   @{text "> \"BAR\" :: \"'a\""}
   \end{isabelle}
 
-  you do not obtain a constant of type @{typ nat}, but a free variable (printed in 
-  blue) of polymorphic type. The problem is that the ML-expression above did 
-  not register the declaration with the current theory. This is what the command
-  \isacommand{setup} is for. The constant is properly declared with
+  you can see that you do not obtain a constant of type @{typ nat}, but a free 
+  variable (printed in blue) of polymorphic type. The problem is that the 
+  ML-expression above did not ``register'' the declaration with the current theory. 
+  This is what the command \isacommand{setup} is for. The constant is properly 
+  declared with
 *}
 
-setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
+setup %gray {* Sign.declare_const @{context} 
+  ((@{binding "BAR"}, @{typ "nat"}), NoSyn) #> snd *}
 
 text {* 
   Now 
@@ -116,7 +118,7 @@
   @{text "> \"BAR\" :: \"nat\""}
   \end{isabelle}
 
-  returns a (black) constant with the type @{typ nat}.
+  returns a (black) constant with the type @{typ nat}, as expected.
 
   A similar command is \isacommand{local\_setup}, which expects a function
   of type @{ML_type "local_theory -> local_theory"}. Later on we will also
diff -r 69b5ba7518b9 -r 490fe9483c0d ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Thu Nov 03 17:53:36 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Fri Nov 04 09:29:50 2011 +0000
@@ -1251,6 +1251,8 @@
   theories, and therefore one can access the data potentially 
   indefinitely.
 
+  Move elsewhere
+
   For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, 
   for treating theories and proof contexts more uniformly. This type is defined as follows
 *}
diff -r 69b5ba7518b9 -r 490fe9483c0d progtutorial.pdf
Binary file progtutorial.pdf has changed