changeset 91 | 667a0943c40b |
child 110 | 12533bb49615 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Package/Ind_Code.thy Thu Jan 29 17:09:56 2009 +0000 @@ -0,0 +1,22 @@ +theory Ind_Code +imports "../Base" Simple_Inductive_Package +begin + +text {* + + @{ML_chunk [display,gray] induction_rules} + +*} + +text {* + + @{ML_chunk [display,gray] intro_rules} + +*} + +text {* + + @{ML_chunk [display,gray] storing} + +*} +end