isabelle: src/HOL/Cardinals/Cardinals.thy@78698a97afb3 (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	9	section \<open>Theory of Ordinals and Cardinals\<close>
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
	Sun, 12 Nov 2023 12:54:26 +0100
changeset 78959	78698a97afb3
parent 63167	0909deb8059b
permissions	-rw-r--r--