changeset 16417 | 9bc16273c2d4 |
parent 14046 | 6616e6c53d48 |
child 35762 | af3ff2ba4c54 |
--- a/src/ZF/Cardinal_AC.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/ZF/Cardinal_AC.thy Fri Jun 17 16:12:49 2005 +0200 @@ -8,7 +8,7 @@ header{*Cardinal Arithmetic Using AC*} -theory Cardinal_AC = CardinalArith + Zorn: +theory Cardinal_AC imports CardinalArith Zorn begin subsection{*Strengthened Forms of Existing Theorems on Cardinals*}