--- a/src/HOL/Inductive.thy Tue Jun 30 20:50:34 1998 +0200 +++ b/src/HOL/Inductive.thy Tue Jun 30 20:51:15 1998 +0200 @@ -1,3 +1,4 @@ -Inductive = Gfp + Prod + Sum + "indrule" +Inductive = Gfp + Prod + Sum + +end