diff -r c3fe4749ef01 -r 83cea5dc6bac CookBook/Recipes/StoringData.thy --- 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) *}