src/HOL/ROOT.ML
changeset 21246 e0e555b67fe5
parent 19835 81d6dc597559
child 21909 a6439243512b
     1.1 --- a/src/HOL/ROOT.ML	Wed Nov 08 13:48:34 2006 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Nov 08 13:48:35 2006 +0100
     1.3 @@ -37,6 +37,11 @@
     1.4  
     1.5  with_path "Integ" use_thy "Main";
     1.6  
     1.7 +structure Main =
     1.8 +struct
     1.9 +  val thy = theory "Main"
    1.10 +end;
    1.11 +
    1.12  path_add "~~/src/HOL/Library";
    1.13  
    1.14  Goal "True";  (*leave subgoal package empty*)