CookBook/Package/Ind_Code.thy
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