changeset 6888 | d0c68ebdabc5 |
parent 6783 | 9cf9c17d9e35 |
child 6954 | dbeafc269f4f |
--- 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";