From 76d6b0b2b1f039549d308a0d2c478a6b05869af9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 24 Jul 2008 09:51:53 +0000
Subject: Merge changes from Version4Branch.

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

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

diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy
new file mode 100644
index 00000000..2eee4f18
--- /dev/null
+++ b/isar/Example-Tokens.thy
@@ -0,0 +1,34 @@
+(*
+      Example proof document for Isabelle/Isar Proof General,
+      using symbols.  
+      View and process this document with Unicode Tokens engaged.
+   
+      $Id$
+*)
+
+theory "Example-Xsym" imports Main begin
+
+text {* Proper proof text -- \<^bitalic>naive version\<^eitalic>. *}
+
+theorem and_comms: "\<phi> \<and> \<psi> \<longrightarrow> \<psi> \<and> \<phi>"
+proof
+   assume "\<phi> \<and> \<psi>"
+  then show "\<psi> \<and> \<phi>"
+  proof
+    assume \<psi> and \<phi>
+    then show ?thesis ..
+ qed
+qed
+
+text {* \<^bbold>Unstructured\<^ebold> proof script. *}
+
+theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> (\<phi>\<^isub>\<beta>  ∧  \<phi>\<^isub>\<alpha>)"
+  apply (rule impI)
+  apply (erule conjE)
+  apply (rule conjI)
+  apply assumption
+  apply assumption
+done
+
+end
+
-- 
cgit v1.2.3