CookBook/Package/Ind_Code.thy
changeset 91 667a0943c40b
child 110 12533bb49615
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Package/Ind_Code.thy	Thu Jan 29 17:09:56 2009 +0000
@@ -0,0 +1,22 @@
+theory Ind_Code
+imports "../Base" Simple_Inductive_Package
+begin
+
+text {*
+
+  @{ML_chunk [display,gray] induction_rules}
+
+*}
+
+text {*
+
+  @{ML_chunk [display,gray] intro_rules}
+
+*}
+
+text {*
+
+  @{ML_chunk [display,gray] storing}
+
+*}
+end