diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-02-19 12:09:38 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-02-19 12:09:38 +0000 |
| commit | a6f7c0c9a31778993267c0ba4231d36ac2ae2a62 (patch) | |
| tree | ce0bde11a06f7e66d1834f4d5bbbce3e15d18e03 /etc/isar/Depends.thy | |
| parent | 678dbb1404401825fcb427a5bb29512c287caa42 (diff) | |
New files.
Diffstat (limited to 'etc/isar/Depends.thy')
| -rw-r--r-- | etc/isar/Depends.thy | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/etc/isar/Depends.thy b/etc/isar/Depends.thy new file mode 100644 index 00000000..d69e663d --- /dev/null +++ b/etc/isar/Depends.thy @@ -0,0 +1,16 @@ +(* In order to test the latest thm deps setup, consider this example: *) + +theory Depends = Main: + + lemma I: "A ==> A" and K: "A ==> B ==> A" . + +(* +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 + |