# HG changeset patch # User lcp # Date 783620082 -3600 # Node ID 661fc2e9c9458b897c4452f363e8ba21eacf3cea # Parent 4d9f6d83c2bf411971dd388686e798b860e2474a FOL/ex/ROOT: now loads mini.ML diff -r 4d9f6d83c2bf -r 661fc2e9c945 src/FOL/ex/ROOT.ML --- a/src/FOL/ex/ROOT.ML Mon Oct 31 17:09:10 1994 +0100 +++ b/src/FOL/ex/ROOT.ML Mon Oct 31 17:14:42 1994 +0100 @@ -25,6 +25,7 @@ time_use "ex/quant.ML"; writeln"\n** Classical examples **\n"; +time_use "ex/mini.ML"; time_use "ex/cla.ML"; time_use_thy "ex/If";