From 8a2d89a5ad6df65aeaa6c83c0b5bb9609a69c977 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 1 Dec 2009 10:01:18 +0000
Subject: Add test case

---
 etc/trac/trac-307.thy | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 etc/trac/trac-307.thy

(limited to 'etc/trac')

diff --git a/etc/trac/trac-307.thy b/etc/trac/trac-307.thy
new file mode 100644
index 00000000..b4d69be2
--- /dev/null
+++ b/etc/trac/trac-307.thy
@@ -0,0 +1,15 @@
+
+theory trac307 imports Main begin
+
+lemma foo: "Suc x = Suc x" ..
+
+(* 2. Go to the simp-command that does not terminate
+   3. Perform the following actions:
+      Undo, Interrupt, Undo, Next
+   Sync is lost.
+*)
+
+lemma "P (Suc x)" apply (simp add: foo)
+
+end
+
-- 
cgit v1.2.3