changeset 16483 | ace3c2b95353 |
parent 16019 | 0e1405402d53 |
child 16562 | b74143e10410 |
--- a/src/HOL/ROOT.ML Mon Jun 20 22:13:55 2005 +0200 +++ b/src/HOL/ROOT.ML Mon Jun 20 22:13:56 2005 +0200 @@ -9,8 +9,6 @@ val banner = "Higher-Order Logic"; writeln banner; -print_depth 1; - (*old-style theory syntax*) use "thy_syntax.ML"; @@ -40,8 +38,6 @@ path_add "~~/src/HOL/Library"; -print_depth 8; - Goal "True"; (*leave subgoal package empty*) val HOL_proofs = !proofs;