use induct_rulify2;
authorwenzelm
Wed Oct 31 01:21:01 2001 +0100 (2001-10-31)
changeset 11990c1daefc08eff
parent 11989 d4bcba4e080e
child 11991 da6ee05d9f3d
use induct_rulify2;
src/HOL/Inductive.thy
     1.1 --- a/src/HOL/Inductive.thy	Wed Oct 31 01:20:42 2001 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Oct 31 01:21:01 2001 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4    imp_conv_disj not_not de_Morgan_disj de_Morgan_conj
     1.5    not_all not_ex
     1.6    Ball_def Bex_def
     1.7 -  inductive_rulify2
     1.8 +  induct_rulify2
     1.9  
    1.10  
    1.11  subsubsection {* Inductive datatypes and primitive recursion *}