From e83e1554aa3eb8fbe8795a4cfec1207cdd0d3ae2 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Fri, 4 Dec 2009 09:42:41 +0000
Subject: New files

---
 etc/isar/Trac280-subrev.thy | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 etc/isar/Trac280-subrev.thy

(limited to 'etc/isar')

diff --git a/etc/isar/Trac280-subrev.thy b/etc/isar/Trac280-subrev.thy
new file mode 100644
index 00000000..2c5984c1
--- /dev/null
+++ b/etc/isar/Trac280-subrev.thy
@@ -0,0 +1,15 @@
+theory Test imports Main begin
+
+lemma 
+ assumes asm: "P\<^isub>i \<and> Q\<^isub>i"
+ shows "Q\<^isub>i \<and> P\<^isub>i"
+proof - 
+  from asm obtain "P\<^isub>i" and "Q\<^isub>i"
+    by blast
+  then show "Q\<^isub>i \<and> P\<^isub>i"
+    by simp
+qed
+
+end
+
+
-- 
cgit v1.2.3