diff options
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 |