Quelle  ROOT   Sprache: Isabelle

chapter AFP

session "Transitive_Models" =  "Delta_System_Lemma" +
  on"
    Transitive Models of Fragments of ZFC

    We extend the ZF-Constructibility library by relativizing theories
    of the Isabelle/ZF and
    class. We also relativize Paulson's work on Aleph and our former
treatmentoftheof Choices. This workis a
    prerrequisite to our formalization of the independence of the
    Continuum Hypothesis.
  "
  options [timeout = 300]
  theories
    "Renaming_Auto"
    "Delta_System_Relative"
    "Pointed_DC_Relative"
    Partial_Functions_Relative
  document_files
    "root.tex"
    "root.bib"
    "root.bst"