isabelle: src/HOL/Finite.thy@8c9fadda81f4 (annotated)

1475 7f5a4cd08209 expanded tabs; renamed subtype to typedef; clasohm parents: 1370 diff changeset	1	(* Title: HOL/Finite.thy
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	3	Author: Lawrence C Paulson & Tobias Nipkow
e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	4	Copyright 1995 University of Cambridge & TU Muenchen
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	6	Finite sets and their cardinality
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
5101 52e7c75acfe6 Adapted to new inductive package. berghofe parents: 3413 diff changeset	9	Finite = Divides + Power + Inductive +
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	10
3413 c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	11	consts Finites :: 'a set set
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	12
3413 c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	13	inductive "Finites"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	intrs
3413 c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	15	emptyI "{} : Finites"
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	16	insertI "A : Finites ==> insert a A : Finites"
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	17
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	18	syntax finite :: 'a set => bool
c1f63cc3a768 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. nipkow parents: 3389 diff changeset	19	translations "finite A" == "A : Finites"
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	20
1556 2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	21	constdefs
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	22	card :: 'a set => nat
2fd82cec17d4 added constdefs section clasohm parents: 1531 diff changeset	23	"card A == LEAST n. ? f. A = {f i \|i. i<n}"
1531 e5eb247ad13c Added a constant UNIV == {x.True} nipkow parents: 1475 diff changeset	24
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	25	end

author	paulson
	Tue, 18 Aug 1998 10:24:54 +0200
changeset 5330	8c9fadda81f4
parent 5101	52e7c75acfe6
child 5616	497eeeace3fc
permissions	-rw-r--r--