# 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