--- a/src/HOL/Finite.thy Wed Mar 06 14:11:41 1996 +0100
+++ b/src/HOL/Finite.thy Wed Mar 06 14:12:24 1996 +0100
@@ -15,10 +15,12 @@
emptyI "{} : Fin(A)"
insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)"
-consts finite :: 'a set => bool
-defs finite_def "finite A == A : Fin(UNIV)"
+constdefs
-consts card :: 'a set => nat
-defs card_def "card A == LEAST n. ? f. A = {f i |i. i<n}"
+ finite :: 'a set => bool
+ "finite A == A : Fin(UNIV)"
+
+ card :: 'a set => nat
+ "card A == LEAST n. ? f. A = {f i |i. i<n}"
end