src/HOL/ROOT.ML
changeset 21246 e0e555b67fe5
parent 19835 81d6dc597559
child 21909 a6439243512b
equal deleted inserted replaced
21245:23e6eb4d0975 21246:e0e555b67fe5
    35 use "~~/src/Provers/quasi.ML";
    35 use "~~/src/Provers/quasi.ML";
    36 use "~~/src/Provers/order.ML";
    36 use "~~/src/Provers/order.ML";
    37 
    37 
    38 with_path "Integ" use_thy "Main";
    38 with_path "Integ" use_thy "Main";
    39 
    39 
       
    40 structure Main =
       
    41 struct
       
    42   val thy = theory "Main"
       
    43 end;
       
    44 
    40 path_add "~~/src/HOL/Library";
    45 path_add "~~/src/HOL/Library";
    41 
    46 
    42 Goal "True";  (*leave subgoal package empty*)
    47 Goal "True";  (*leave subgoal package empty*)
    43 
    48 
    44 val HOL_proofs = !proofs;
    49 val HOL_proofs = !proofs;