src/HOL/Isar_examples/ROOT.ML
changeset 12946 75447c743810
parent 12105 1e4451999200
child 16356 94011cf701a4
equal deleted inserted replaced
12945:95853fbcc718 12946:75447c743810
    11 time_use_thy "ExprCompiler";
    11 time_use_thy "ExprCompiler";
    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 "../W0" (no_document time_use_thy) "Type";
       
    17 with_path "../W0" time_use_thy "W_correct";
       
    18 with_path "../NumberTheory" (no_document time_use_thy) "Primes";
    16 with_path "../NumberTheory" (no_document time_use_thy) "Primes";
    19 with_path "../NumberTheory" time_use_thy "Fibonacci";
    17 with_path "../NumberTheory" time_use_thy "Fibonacci";
    20 time_use_thy "Puzzle";
    18 time_use_thy "Puzzle";
    21 time_use_thy "NestedDatatype";
    19 time_use_thy "NestedDatatype";
    22 time_use_thy "HoareEx";
    20 time_use_thy "HoareEx";