# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274113641 -3600
# Node ID 0a25b35178c33af23f3e616a2628838d6fbdbcf5
# Parent  e79563b14b0fd2168b53f8026f9dcfda054b7c3b
updated to new isabelle

diff -r e79563b14b0f -r 0a25b35178c3 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Mon Apr 26 05:20:01 2010 +0200
+++ b/ProgTutorial/Base.thy	Mon May 17 17:27:21 2010 +0100
@@ -28,7 +28,7 @@
 ML {*
 fun write_file txt thy =
 let 
-  val stream = Config.get_thy thy filename
+  val stream = Config.get_global thy filename
                |> TextIO.openAppend 
 in
   TextIO.output (stream, txt); 
@@ -73,7 +73,7 @@
   val _ = tracing ("Open File: " ^ name)
   val _ = TextIO.openOut name
 in 
-  Config.put_thy filename name thy
+  Config.put_global filename name thy
 end
 *}
 
diff -r e79563b14b0f -r 0a25b35178c3 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Mon Apr 26 05:20:01 2010 +0200
+++ b/ProgTutorial/Essential.thy	Mon May 17 17:27:21 2010 +0100
@@ -1082,7 +1082,7 @@
   manipulated as a configuration value:
 
   @{ML_response_fake [display,gray]
-  "Config.get_thy @{theory} (Unify.search_bound_value)"
+  "Config.get_global @{theory} (Unify.search_bound_value)"
   "Int 60"}
 
   If this bound is reached during unification, Isabelle prints out the
diff -r e79563b14b0f -r 0a25b35178c3 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Apr 26 05:20:01 2010 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon May 17 17:27:21 2010 +0100
@@ -1378,15 +1378,15 @@
   "Config.get @{context} bval" 
   "true"}
 
-  or directly from a theory using the function @{ML_ind get_thy in Config}
+  or directly from a theory using the function @{ML_ind get_global in Config}
 
   @{ML_response [display,gray] 
-  "Config.get_thy @{theory} bval" 
+  "Config.get_global @{theory} bval" 
   "true"}
 
   It is also possible to manipulate the configuration values
   from the ML-level with the functions @{ML_ind put in Config}
-  and @{ML_ind put_thy in Config}. For example
+  and @{ML_ind put_global in Config}. For example
 
   @{ML_response [display,gray]
   "let
diff -r e79563b14b0f -r 0a25b35178c3 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Mon Apr 26 05:20:01 2010 +0200
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Mon May 17 17:27:21 2010 +0100
@@ -195,5 +195,22 @@
 ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
+ML{*fun pat_completeness_auto ctxt =
+  Pat_Completeness.pat_completeness_tac ctxt 1
+    THEN auto_tac (clasimpset_of ctxt)*}
+
+ML {*
+  val conf = Function_Common.default_config
+*}
+
+datatype foo = Foo nat
+
+local_setup{*Primrec.add_primrec [(@{binding "bar"}, NONE, NoSyn)] 
+    [(Attrib.empty_binding, @{term "\<And>x. bar (Foo x) = x"})]
+  #> snd *}
+
+local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 
+    [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]
+      conf pat_completeness_auto #> snd*}
 
 (*<*)end(*>*)
\ No newline at end of file
diff -r e79563b14b0f -r 0a25b35178c3 progtutorial.pdf
Binary file progtutorial.pdf has changed