From 28748c6c9f1ee178595b0e0c517fe9dfca1184ed Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 Jan 2008 20:38:11 +0000
Subject: New files.

---
 etc/isar/Trac189.thy | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 etc/isar/Trac189.thy

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
-- 
cgit v1.2.3