--- a/src/HOL/Finite.thy Mon Nov 27 13:44:56 1995 +0100 +++ b/src/HOL/Finite.thy Wed Nov 29 16:44:59 1995 +0100 @@ -7,7 +7,7 @@ *) Finite = Lfp + -consts Fin :: "'a set => 'a set set" +consts Fin :: 'a set => 'a set set inductive "Fin(A)" intrs