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} *}