author | wenzelm |
Wed, 31 Oct 2001 01:21:01 +0100 | |
changeset 11990 | c1daefc08eff |
parent 11989 | d4bcba4e080e |
child 11991 | da6ee05d9f3d |
--- 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 *}