Nominal/ROOT.ML
changeset 2734 eee5deb35aa8
parent 2646 51f75d24bd73
child 2926 37c0d7953cba
equal deleted inserted replaced
2733:5f6fefdbf055 2734:eee5deb35aa8
     1 
     1 
     2 
     2 
     3 no_document use_thys
     3 no_document use_thys
     4    ["Atoms",
     4    ["Atoms",
       
     5     "Eqvt",
     5     "Ex/Weakening",
     6     "Ex/Weakening",
     6     "Ex/Classical",    
     7     "Ex/Classical",    
     7     "Ex/Datatypes",
     8     "Ex/Datatypes",
     8     "Ex/Ex1",
     9     "Ex/Ex1",
     9     "Ex/ExPS3",
    10     "Ex/ExPS3",