Merge changes from Version4Branch.

1 files changed, 0 insertions, 42 deletions

diff --git a/isar/Example-Xsym.thy b/isar/Example-Xsym.thy
deleted file mode 100644
index b864428f..00000000
--- a/isar/Example-Xsym.thy
+++ /dev/null
@@ -1,42 +0,0 @@
-(*
-      Example proof document for Isabelle/Isar Proof General.
-   
-      $Id$
-*)
-
-theory "Example-Xsym" imports Main begin
-
-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 \<and> 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