author | wenzelm |
Thu, 07 Sep 2006 15:16:41 +0200 | |
changeset 20489 | a684fc70d04e |
parent 20488 | 121bc2135bd3 |
child 20490 | e502690952be |
--- a/doc-src/IsarImplementation/Thy/ML.thy Thu Sep 07 15:16:26 2006 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Sep 07 15:16:41 2006 +0200 @@ -15,4 +15,11 @@ text {* FIXME beyond the basis library definition *} + +chapter {* Cookbook *} + +section {* Defining a method that depends on declarations in the context *} + +text FIXME + end