# HG changeset patch # User wenzelm # Date 928518807 -7200 # Node ID 951d5f5c3c9515f2bd894b821691afbfe6f523d8 # Parent 7eb14a4047e3c2062799dda4e8f789487acb5332 added calculation.ML; diff -r 7eb14a4047e3 -r 951d5f5c3c95 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Fri Jun 04 19:53:03 1999 +0200 +++ b/src/Pure/Isar/ROOT.ML Fri Jun 04 19:53:27 1999 +0200 @@ -13,6 +13,7 @@ use "args.ML"; use "attrib.ML"; use "method.ML"; +use "calculation.ML"; (*outer syntax*) use "comment.ML";