Merge changes from Version4Branch.

1 files changed, 34 insertions, 0 deletions

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
+