# HG changeset patch # User paulson # Date 827402676 -3600 # Node ID b9984b1dbc4c5502870ff768256e74513df7c189 # Parent b776e3223dd6958a82d1c8c93adde001e0912840 Now loads deriv.ML diff -r b776e3223dd6 -r b9984b1dbc4c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Mar 20 18:43:08 1996 +0100 +++ b/src/Pure/ROOT.ML Thu Mar 21 11:04:36 1996 +0100 @@ -35,6 +35,8 @@ use "logic.ML"; use "theory.ML"; use "thm.ML"; +use "deriv.ML"; +use "display.ML"; use "drule.ML"; use "tctical.ML"; use "search.ML";