theory Ind_Codeimports "../Base" Simple_Inductive_Packagebegintext {* @{ML_chunk [display,gray] definitions_aux} @{ML_chunk [display,gray,linenos] definitions}*}text {* @{ML_chunk [display,gray] induction_rules}*}text {* @{ML_chunk [display,gray] intro_rules}*}text {* Things to include at the end: \begin{itemize} \item say something about add-inductive-i to return the rules \item say that the induction principle is weaker (weaker than what the standard inductive package generates) \end{itemize}*}end