diff -r 2b07da8b310d -r 1c17e99f6f66 CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Wed Oct 01 20:09:45 2008 -0400 +++ b/CookBook/Recipes/NamedThms.thy Wed Oct 01 20:42:55 2008 -0400 @@ -28,7 +28,7 @@ text {* This declares a context data slot where the theorems are stored, an attribute @{attribute foo} (with the usual @{text add} and @{text del} options - to declare new rules, and the internal ML interface to retrieve and + to declare new rules) and the internal ML interface to retrieve and modify the facts. Furthermore, the facts are made available under the dynamic fact name