# HG changeset patch # User wenzelm # Date 1157635001 -7200 # Node ID a684fc70d04e5899138aa588ae57d2ec200cc776 # Parent 121bc2135bd3a6a2fc834f18f0f58b396970be88 tentative appendix C; diff -r 121bc2135bd3 -r a684fc70d04e doc-src/IsarImplementation/Thy/ML.thy --- 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