src/HOL/ROOT.ML
changeset 21909 a6439243512b
parent 21246 e0e555b67fe5
child 22946 9793d28d49ad
     1.1 --- a/src/HOL/ROOT.ML	Wed Dec 27 19:09:57 2006 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Dec 27 19:09:58 2006 +0100
     1.3 @@ -37,11 +37,6 @@
     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*)