--- a/src/HOL/Inductive.thy Wed Jul 01 11:20:32 1998 +0200 +++ b/src/HOL/Inductive.thy Wed Jul 01 11:33:39 1998 +0200 @@ -1,4 +1,2 @@ -Inductive = Gfp + Prod + Sum + -end - +Inductive = Gfp + Prod + Sum