theory Ind_Code
imports "../Base" Simple_Inductive_Package
begin

text {*
  What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK?
*}


text {*

  @{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