equal
deleted
inserted
replaced
739 session "HOL-Cardinals" in Cardinals = HOL + |
739 session "HOL-Cardinals" in Cardinals = HOL + |
740 description {* |
740 description {* |
741 Ordinals and Cardinals, Full Theories. |
741 Ordinals and Cardinals, Full Theories. |
742 *} |
742 *} |
743 options [document = false] |
743 options [document = false] |
744 theories Cardinals |
744 theories |
|
745 Cardinals |
|
746 Bounded_Set |
745 document_files |
747 document_files |
746 "intro.tex" |
748 "intro.tex" |
747 "root.tex" |
749 "root.tex" |
748 "root.bib" |
750 "root.bib" |
749 |
751 |