diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/Package/Ind_Code.thy
--- a/CookBook/Package/Ind_Code.thy	Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy	Sat Feb 14 13:20:21 2009 +0000
@@ -4,6 +4,13 @@
 
 text {*
 
+  @{ML_chunk [display,gray] definitions_aux}
+  @{ML_chunk [display,gray,linenos] definitions}
+
+*}
+
+text {*
+
   @{ML_chunk [display,gray] induction_rules}
 
 *}