| changeset 18456 | 8cc35e95450a |
| parent 17009 | 932e0e370926 |
| child 19599 | a5c7eb37d14f |
--- a/src/HOL/Inductive.thy Wed Dec 21 17:00:57 2005 +0100 +++ b/src/HOL/Inductive.thy Thu Dec 22 00:28:34 2005 +0100 @@ -67,7 +67,7 @@ imp_conv_disj not_not de_Morgan_disj de_Morgan_conj not_all not_ex Ball_def Bex_def - induct_rulify2 + induct_rulify_fallback subsection {* Inductive datatypes and primitive recursion *}