src/HOL/Isar_examples/ROOT.ML
changeset 6882 fe4e3d26fa8f
parent 6765 6eba3d69037b
child 7384 33c976216121
equal deleted inserted replaced
6881:91a2c8b8269a 6882:fe4e3d26fa8f
     9 use_thy "Peirce";
     9 use_thy "Peirce";
    10 use_thy "Cantor";
    10 use_thy "Cantor";
    11 use_thy "ExprCompiler";
    11 use_thy "ExprCompiler";
    12 use_thy "Group";
    12 use_thy "Group";
    13 use_thy "NatSum";
    13 use_thy "NatSum";
       
    14 use_thy "KnasterTarski";