--- 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