src/ZF/ROOT.ML
changeset 23146 0bc590051d95
parent 17935 c6f1442ce949
child 23168 fcdd4346fa6b
     1.1 --- a/src/ZF/ROOT.ML	Thu May 31 11:00:06 2007 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Thu May 31 12:06:31 2007 +0200
     1.3 @@ -13,6 +13,6 @@
     1.4  
     1.5  reset eta_contract;
     1.6  
     1.7 -with_path "Integ" use_thy "Main_ZFC";
     1.8 +use_thy "Main_ZFC";
     1.9  
    1.10  Goal "True";  (*leave subgoal package empty*)