# HG changeset patch
# User wenzelm
# Date 1004487661 -3600
# Node ID c1daefc08eff1789181299e72bd8bc8c08f48068
# Parent  d4bcba4e080e02a915f94294479dbc0fd6fc202f
use induct_rulify2;

diff -r d4bcba4e080e -r c1daefc08eff src/HOL/Inductive.thy
--- 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 *}