isabelle: src/HOL/Cardinals/Cardinals.thy@8f4a332500e4 (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
55102 761e40ce91bc whitespace tuning blanchet parents: 54980 diff changeset	9	header {* 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
	Mon, 18 Aug 2014 12:17:31 +0200
changeset 57978	8f4a332500e4
parent 55102	761e40ce91bc
child 58889	5b7a9633cfa8
permissions	-rw-r--r--