src/Pure/Isar/ROOT.ML
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";