changeset 20491 | 98ba42f19995 |
parent 20489 | a684fc70d04e |
child 20520 | 05fd007bdeb9 |
--- a/doc-src/IsarImplementation/Thy/ML.thy Thu Sep 07 15:16:51 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Sep 07 20:12:08 2006 +0200 @@ -18,7 +18,7 @@ chapter {* Cookbook *} -section {* Defining a method that depends on declarations in the context *} +section {* A method that depends on declarations in the context *} text FIXME