# HG changeset patch # User wenzelm # Date 938026979 -7200 # Node ID 594f09166c38e1f40e524dbaad8d39b61b37fc82 # Parent e1e2d07287d8e5546275f6a55eed0a0bce890b0d tuned; diff -r e1e2d07287d8 -r 594f09166c38 src/FOL/ROOT.ML --- a/src/FOL/ROOT.ML Wed Sep 22 21:02:32 1999 +0200 +++ b/src/FOL/ROOT.ML Wed Sep 22 21:02:59 1999 +0200 @@ -21,7 +21,6 @@ use "~~/src/Provers/clasimp.ML"; use "~~/src/Provers/quantifier1.ML"; -use_thy "IFOL"; use_thy "FOL"; print_depth 8;