src/HOL/ROOT
changeset 59747 7325ffa35038
parent 59743 d8fb00487c4d
child 59777 9ad96e97e72d
equal deleted inserted replaced
59746:ddae5727c5a9 59747:7325ffa35038
   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