Nominal/ROOT.ML
changeset 3075 31d51ce547b7
parent 3046 9b0324e1293b
child 3097 b27e94db1b8a
equal deleted inserted replaced
3066:da60dc911055 3075:31d51ce547b7
    30    ];
    30    ];
    31 
    31 
    32 quick_and_dirty := true;
    32 quick_and_dirty := true;
    33 
    33 
    34 no_document use_thys
    34 no_document use_thys
    35    ["Ex/Classical",    
    35    ["Ex/Let"];
    36     "Ex/Let"
       
    37    ];
       
    38 
    36 
    39 
    37