685 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" + |
685 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" + |
686 options [timeout = 3600, condition = ISABELLE_POLYML, document = false] |
686 options [timeout = 3600, condition = ISABELLE_POLYML, document = false] |
687 theories Nominal_Examples |
687 theories Nominal_Examples |
688 theories [quick_and_dirty] VC_Condition |
688 theories [quick_and_dirty] VC_Condition |
689 |
689 |
690 session "HOL-Cardinals-Base" in Cardinals = HOL + |
690 session "HOL-Cardinals-LFP" in Cardinals = HOL + |
691 description {* |
691 description {* |
692 Ordinals and Cardinals, Base Theories. |
692 Ordinals and Cardinals, Theories Needed for BNF LFP Construction. |
693 *} |
693 *} |
694 options [document = false] |
694 options [document = false] |
695 theories Cardinal_Arithmetic |
695 theories Cardinal_Arithmetic |
696 |
696 |
697 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" + |
697 session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-LFP" + |
698 description {* |
698 description {* |
699 Ordinals and Cardinals, Full Theories. |
699 Ordinals and Cardinals, Full Theories. |
700 *} |
700 *} |
701 options [document = false] |
701 options [document = false] |
702 theories Cardinals |
702 theories Cardinals |
703 files |
703 files |
704 "document/intro.tex" |
704 "document/intro.tex" |
705 "document/root.tex" |
705 "document/root.tex" |
706 "document/root.bib" |
706 "document/root.bib" |
707 |
707 |
708 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" + |
708 session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-LFP" + |
709 description {* |
709 description {* |
710 Bounded Natural Functors for Datatypes. |
710 Bounded Natural Functors for Datatypes. |
711 *} |
711 *} |
712 options [document = false] |
712 options [document = false] |
713 theories BNF_LFP |
713 theories BNF_LFP |