src/HOL/Isar_examples/ROOT.ML
changeset 7621 4074bc1e380d
parent 7443 e5356e73f57a
child 7800 8ee919e42174
equal deleted inserted replaced
7620:8d721c3f4acb 7621:4074bc1e380d
    12 time_use_thy "Group";
    12 time_use_thy "Group";
    13 time_use_thy "Summation";
    13 time_use_thy "Summation";
    14 time_use_thy "KnasterTarski";
    14 time_use_thy "KnasterTarski";
    15 time_use_thy "MutilatedCheckerboard";
    15 time_use_thy "MutilatedCheckerboard";
    16 with_path "../Induct" time_use_thy "MultisetOrder";
    16 with_path "../Induct" time_use_thy "MultisetOrder";
       
    17 with_path "../W0" time_use_thy "W_correct";