changeset 11990 | c1daefc08eff |
parent 11825 | ef7d619e2c88 |
child 12023 | d982f98e0f0d |
--- a/src/HOL/Inductive.thy Wed Oct 31 01:20:42 2001 +0100 +++ b/src/HOL/Inductive.thy Wed Oct 31 01:21:01 2001 +0100 @@ -62,7 +62,7 @@ imp_conv_disj not_not de_Morgan_disj de_Morgan_conj not_all not_ex Ball_def Bex_def - inductive_rulify2 + induct_rulify2 subsubsection {* Inductive datatypes and primitive recursion *}