From f26d9fd4b9886082435d076004eeebdfeea2ef4b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 24 Sep 2003 23:41:44 +0000
Subject: New files.

---
 isar/Example-Xsym.thy | 43 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 isar/Example-Xsym.thy

(limited to 'isar/Example-Xsym.thy')

diff --git a/isar/Example-Xsym.thy b/isar/Example-Xsym.thy
new file mode 100644
index 00000000..c731143b
--- /dev/null
+++ b/isar/Example-Xsym.thy
@@ -0,0 +1,43 @@
+(*
+      Example proof document for Isabelle/Isar Proof General.
+   
+      $Id$
+*)
+
+theory Example = Main:
+
+text {* Proper proof text -- \textit{naive version}. *}
+
+theorem and_comms: "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A \<and> B"
+  then show "B \<and> A"
+  proof
+    assume B and A
+    then
+   show ?thesis ..
+ qed
+qed
+
+
+text {* Proper proof text -- \textit{advanced version}. *}
+
+theorem "A \<and> B \<longrightarrow> B \<and> A"
+proof
+  assume "A & B"
+  then obtain B and A ..
+  then show "B \<and> A" ..
+qed
+
+
+text {* Unstructured proof script. *}
+
+theorem "A \<and> B \<longrightarrow> B \<and> A"
+  apply (rule impI)
+  apply (erule conjE)
+  apply (rule conjI)
+  apply assumption
+  apply assumption
+done
+
+end
-- 
cgit v1.2.3