isabelle: src/HOL/Cardinals/Cardinals.thy@5ae2a2e74c93 (annotated)

49439 80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	1	(* Title: HOL/Cardinals/Cardinals.thy
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	2	Author: Andrei Popescu, TU Muenchen
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	3	Author: Dmitriy Traytel, TU Muenchen
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	4	Copyright 2012
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	5
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	6	Theory of ordinals and cardinals.
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	7	*)
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	8
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 55102 diff changeset	9	section {* Theory of Ordinals and Cardinals *}
49439 80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	10
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	11	theory Cardinals
54980 7e0573a490ee basic ordinal arithmetic and cardinals library extension (not relevant for BNFs) traytel parents: 54545 diff changeset	12	imports Ordinal_Arithmetic Cardinal_Arithmetic Wellorder_Extension
49439 80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	13	begin
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	14
80b1963215c8 added top-level theory for Cardinals popescua parents: diff changeset	15	end

author	wenzelm
	Sat, 23 May 2015 17:19:37 +0200
changeset 60299	5ae2a2e74c93
parent 58889	5b7a9633cfa8
child 63167	0909deb8059b
permissions	-rw-r--r--