| changeset 16483 | ace3c2b95353 |
| parent 15481 | fc075ae929e4 |
| child 17935 | c6f1442ce949 |
--- a/src/ZF/ROOT.ML Mon Jun 20 22:13:55 2005 +0200 +++ b/src/ZF/ROOT.ML Mon Jun 20 22:13:56 2005 +0200 @@ -13,13 +13,9 @@ reset eta_contract; -print_depth 1; - (*syntax for old-style theory sections*) use "thy_syntax"; with_path "Integ" use_thy "Main_ZFC"; -print_depth 8; - Goal "True"; (*leave subgoal package empty*)