Nominal/ROOT.ML
changeset 2330 8728f7990f6d
parent 2288 3b83960f9544
child 2440 0a36825b16c1
equal deleted inserted replaced
2329:df3a952c6a67 2330:8728f7990f6d
     1 quick_and_dirty := true;
     1 quick_and_dirty := true;
     2 
     2 
       
     3 (*
     3 no_document use_thys
     4 no_document use_thys
     4    ["Ex/Lambda",
     5    ["Ex/Lambda",
     5     "Ex/LF",
     6     "Ex/LF",
     6     "Ex/SingleLet",
     7     "Ex/SingleLet",
     7     "Ex/Ex1rec",
     8     "Ex/Ex1rec",
    15     "Ex/ExPS7",
    16     "Ex/ExPS7",
    16     "Ex/CoreHaskell",
    17     "Ex/CoreHaskell",
    17     "Ex/Test"(*,
    18     "Ex/Test"(*,
    18     "Manual/Term4"*)
    19     "Manual/Term4"*)
    19     ];
    20     ];
       
    21 *)