diff -r b071a0b88298 -r 667a0943c40b CookBook/Package/Ind_Code.thy --- /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