src/HOL/ROOT
changeset 61525 87244a9cfe40
parent 61514 213556e498c2
child 61542 b3eb789616c3
equal deleted inserted replaced
61524:f2e51e704a96 61525:87244a9cfe40
   172 session "HOL-Data_Structures" in Data_Structures = HOL +
   172 session "HOL-Data_Structures" in Data_Structures = HOL +
   173   options [document_variants = document]
   173   options [document_variants = document]
   174   theories [document = false]
   174   theories [document = false]
   175     "Less_False"
   175     "Less_False"
   176   theories
   176   theories
   177     Tree_Set
       
   178     Tree_Map
   177     Tree_Map
   179     AVL_Map
   178     AVL_Map
   180     RBT_Map
   179     RBT_Map
   181     Tree23_Map
   180     Tree23_Map
   182     Tree234_Map
   181     Tree234_Map
       
   182     Splay_Map
   183   document_files "root.tex" "root.bib"
   183   document_files "root.tex" "root.bib"
   184 
   184 
   185 session "HOL-Import" in Import = HOL +
   185 session "HOL-Import" in Import = HOL +
   186   theories HOL_Light_Maps
   186   theories HOL_Light_Maps
   187   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import
   187   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import