--- a/src/HOL/Inductive.thy Tue Jul 25 16:52:08 1995 +0200 +++ b/src/HOL/Inductive.thy Tue Jul 25 16:58:06 1995 +0200 @@ -1,1 +1,2 @@ -Inductive = Gfp + Prod +Inductive = Gfp + Prod + Sum +