New files.

1 files changed, 43 insertions, 0 deletions

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