src/HOL/Finite.thy
changeset 1556 2fd82cec17d4
parent 1531 e5eb247ad13c
child 3367 832c245d967c
--- 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