--- a/src/HOL/Inductive.thy Mon Jul 15 14:54:37 1996 +0200 +++ b/src/HOL/Inductive.thy Mon Jul 15 14:58:28 1996 +0200 @@ -1,2 +1,3 @@ -Inductive = Gfp + Prod + Sum +Inductive = Gfp + Prod + Sum + "indrule" +