# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1270631532 -7200
# Node ID 2e199c5faf767697bfb256e659157691efbc2b1f
# Parent  1d1e4cda8c541d3df26d90d18190742ea2039c10
updated to new Isabelle

diff -r 1d1e4cda8c54 -r 2e199c5faf76 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Sun Mar 07 21:15:05 2010 +0100
+++ b/ProgTutorial/Base.thy	Wed Apr 07 11:12:12 2010 +0200
@@ -20,7 +20,7 @@
 (* they also write the code into a separate file  *)
 
 ML {*
-val (filename, setup_filename) = Attrib.config_string "filename" "File_Code.ML"
+val (filename, setup_filename) = Attrib.config_string "filename" (K "File_Code.ML")
 *}
 
 setup {* setup_filename *}
diff -r 1d1e4cda8c54 -r 2e199c5faf76 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Sun Mar 07 21:15:05 2010 +0100
+++ b/ProgTutorial/FirstSteps.thy	Wed Apr 07 11:12:12 2010 +0200
@@ -569,8 +569,8 @@
 *}
 
 setup %gray {* let
-  val (ival1, setup_ival1) = Attrib.config_int "ival1" 1
-  val (ival2, setup_ival2) = Attrib.config_int "ival2" 2
+  val (ival1, setup_ival1) = Attrib.config_int "ival1" (K 1)
+  val (ival2, setup_ival2) = Attrib.config_int "ival2" (K 2)
 in
   setup_ival1 #>
   setup_ival2
@@ -1331,9 +1331,9 @@
   values can be declared by
 *}
 
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
-val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" (K false)
+val (ival, setup_ival) = Attrib.config_int "ival" (K 0)
+val (sval, setup_sval) = Attrib.config_string "sval" (K "some string") *}
 
 text {* 
   where each value needs to be given a default. To enable these values on the 
diff -r 1d1e4cda8c54 -r 2e199c5faf76 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Sun Mar 07 21:15:05 2010 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Wed Apr 07 11:12:12 2010 +0200
@@ -192,7 +192,7 @@
 
 text {* Type declarations *}
 
-ML{*Typedef.add_typedef false NONE (@{binding test},[],NoSyn)
+ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
 
diff -r 1d1e4cda8c54 -r 2e199c5faf76 progtutorial.pdf
Binary file progtutorial.pdf has changed