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+−