CookBook/Package/Ind_Code.thy
changeset 118 5f003fdf2653
parent 110 12533bb49615
child 124 0b9fa606a746
--- 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}
 
 *}