src/HOL/Inductive.thy
changeset 5105 0ff5bec04d02
parent 5102 8c782c25a11e
child 6437 9bdfe07ba8e9
     1.1 --- a/src/HOL/Inductive.thy	Wed Jul 01 11:20:32 1998 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Jul 01 11:33:39 1998 +0200
     1.3 @@ -1,4 +1,2 @@
     1.4 -Inductive = Gfp + Prod + Sum +
     1.5  
     1.6 -end
     1.7 -
     1.8 +Inductive = Gfp + Prod + Sum