# HG changeset patch
# User clasohm
# Date 826117944 -3600
# Node ID 2fd82cec17d403f73e5e2f0884721d74ca890428
# Parent  a5f48457dfd530cb8c4be095d51dece32feaf169
added constdefs section

diff -r a5f48457dfd5 -r 2fd82cec17d4 src/HOL/Finite.thy
--- 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