CookBook/Recipes/StoringData.thy
changeset 63 83cea5dc6bac
parent 61 64c9540f2f84
child 68 e7519207c2b7
--- a/CookBook/Recipes/StoringData.thy	Wed Jan 07 16:36:31 2009 +0000
+++ b/CookBook/Recipes/StoringData.thy	Thu Jan 08 22:46:06 2009 +0000
@@ -2,7 +2,7 @@
 imports "../Base"
 begin
 
-section {* Storing Data *} 
+section {* Storing Data\label{recipe:storingdata} *} 
 
 
 text {*
@@ -16,8 +16,7 @@
 
   *}
 
-ML {*
-local
+ML {* local
 
 structure Data = GenericDataFun
 (
@@ -33,8 +32,7 @@
 
 fun update k v = Data.map (Symtab.update (k, v))
 
-end
-*}
+end *}
 
 setup {* Context.theory_map (update "foo" 1) *}