CookBook/Recipes/NamedThms.thy
changeset 14 1c17e99f6f66
parent 13 2b07da8b310d
child 15 9da9ba2b095b
--- 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