Nominal/ROOT.ML
changeset 2926 37c0d7953cba
parent 2734 eee5deb35aa8
child 3045 d0ad264f8c4f
child 3073 ec31c31b2bb1
equal deleted inserted replaced
2925:b4404b13f775 2926:37c0d7953cba
     2 
     2 
     3 no_document use_thys
     3 no_document use_thys
     4    ["Atoms",
     4    ["Atoms",
     5     "Eqvt",
     5     "Eqvt",
     6     "Ex/Weakening",
     6     "Ex/Weakening",
     7     "Ex/Classical",    
     7     (*"Ex/Classical",*)    
     8     "Ex/Datatypes",
     8     "Ex/Datatypes",
     9     "Ex/Ex1",
     9     "Ex/Ex1",
    10     "Ex/ExPS3",
    10     "Ex/ExPS3",
    11     "Ex/Multi_Recs",
    11     "Ex/Multi_Recs",
    12     "Ex/Multi_Recs2",
    12     "Ex/Multi_Recs2",
    13     "Ex/LF",
    13     "Ex/LF",
    14     "Ex/Lambda",
    14     "Ex/Lambda",
    15     "Ex/Let",
    15     (*"Ex/Let",*)
    16     "Ex/LetPat",
    16     "Ex/LetPat",
    17     "Ex/LetRec",
    17     "Ex/LetRec",
    18     "Ex/LetRec2",
    18     "Ex/LetRec2",
    19     "Ex/LetFun",
    19     "Ex/LetFun",
    20     "Ex/Modules",
    20     "Ex/Modules",
    26     "Ex/Foo1",
    26     "Ex/Foo1",
    27     "Ex/Foo2",
    27     "Ex/Foo2",
    28     "Ex/CoreHaskell",
    28     "Ex/CoreHaskell",
    29     "Ex/CoreHaskell2" 
    29     "Ex/CoreHaskell2" 
    30    ];
    30    ];
       
    31 
       
    32 quick_and_dirty := true;
       
    33 
       
    34 no_document use_thys
       
    35    ["Ex/Classical",    
       
    36     "Ex/Let"
       
    37    ];
       
    38 
       
    39