changeset 124 | 0b9fa606a746 |
parent 118 | 5f003fdf2653 |
child 163 | 2319cff107f0 |
--- a/CookBook/Package/Ind_Code.thy Tue Feb 17 13:53:54 2009 +0000 +++ b/CookBook/Package/Ind_Code.thy Wed Feb 18 17:17:37 2009 +0000 @@ -19,6 +19,20 @@ @{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