ProgTutorial/ROOT.ML
changeset 328 c0cae24b9d46
parent 327 ce754ad78bc9
child 329 5dffcab68680
equal deleted inserted replaced
327:ce754ad78bc9 328:c0cae24b9d46
     1 set quick_and_dirty;
     1 quick_and_dirty := true;
     2 
     2 
     3 no_document use_thy "Base";
     3 no_document use_thy "Base";
     4 no_document use_thy "Package/Simple_Inductive_Package";
     4 no_document use_thy "Package/Simple_Inductive_Package";
     5 
     5 
     6 use_thy "Intro";
     6 use_thy "Intro";