diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-29 20:38:11 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-29 20:38:11 +0000 |
| commit | 28748c6c9f1ee178595b0e0c517fe9dfca1184ed (patch) | |
| tree | ce2d72661c65f62ef2a2e6298fc6b4777f896d1c /etc | |
| parent | 48b353c269908b39fe7efab53f6f95c1a3aa9c2c (diff) | |
New files.
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/isar/Trac189.thy | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/etc/isar/Trac189.thy b/etc/isar/Trac189.thy new file mode 100644 index 00000000..43c4bdd4 --- /dev/null +++ b/etc/isar/Trac189.thy @@ -0,0 +1,8 @@ +theory Trac189 imports Main begin + + +(* Undoing of a diagnostic: exercises proof-no-command *) + +lemma "True" + apply (rule TrueI) + thm TrueI |