diff -r 12b5fb35a688 -r d0c68ebdabc5 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Fri Jul 02 15:05:16 1999 +0200 +++ b/src/Pure/Isar/ROOT.ML Fri Jul 02 19:04:32 1999 +0200 @@ -5,7 +5,7 @@ Isar -- Intelligible Semi-Automated Reasoning for Isabelle. *) -(*proof engine*) +(*basic proof engine*) use "auto_bind.ML"; use "proof_context.ML"; use "proof.ML"; @@ -14,7 +14,10 @@ use "args.ML"; use "attrib.ML"; use "method.ML"; + +(*derived proof elements*) use "calculation.ML"; +use "skip_proof.ML"; (*outer syntax*) use "comment.ML";