theory Ind_Code+
−
imports "../Base" Simple_Inductive_Package+
−
begin+
−
+
−
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+
−