--- a/CookBook/Package/Ind_Code.thy	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy	Sun Mar 08 20:53:00 2009 +0000
@@ -3,6 +3,11 @@
 begin
 
 text {*
+  What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK?
+*}
+
+
+text {*
 
   @{ML_chunk [display,gray] definitions_aux}
   @{ML_chunk [display,gray,linenos] definitions}