aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isar/Depends.thy
diff options
context:
space:
mode:
Diffstat (limited to 'etc/isar/Depends.thy')
-rw-r--r--etc/isar/Depends.thy4
1 files changed, 1 insertions, 3 deletions
diff --git a/etc/isar/Depends.thy b/etc/isar/Depends.thy
index d69e663d..2d13c0f4 100644
--- a/etc/isar/Depends.thy
+++ b/etc/isar/Depends.thy
@@ -1,6 +1,6 @@
(* In order to test the latest thm deps setup, consider this example: *)
-theory Depends = Main:
+theory Depends imports Main begin
lemma I: "A ==> A" and K: "A ==> B ==> A" .
@@ -8,8 +8,6 @@ theory Depends = Main:
This reports I, K depending on several things; for your internal
dependency graph you may interpret this as each member of {I, K} depending
on all the deps.
-
- Markus
*)
end