Tutorial/ROOT.ML
changeset 3133 39c387e690aa
equal deleted inserted replaced
3132:87eca760dcba 3133:39c387e690aa
       
     1 
       
     2 quick_and_dirty := true;
       
     3 
       
     4 no_document use_thys
       
     5    ["Lambda",
       
     6     "Minimal",
       
     7     "Tutorial1s",
       
     8     "Tutorial3s",
       
     9     "Tutorial4s",
       
    10     "Tutorial1",
       
    11     "Tutorial2",
       
    12     "Tutorial2s",
       
    13     "Tutorial3",
       
    14     "Tutorial4",
       
    15     "Tutorial5",
       
    16     "Tutorial6" 
       
    17    ];
       
    18 
       
    19