From fecfbc2d70ab83e3a8dff28229359dc8998fc2d7 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Sun, 3 Aug 2008 20:56:03 +0000
Subject: Fix tokens

---
 isar/Example-Tokens.thy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/isar/Example-Tokens.thy b/isar/Example-Tokens.thy
index 2eee4f18..d9e5ca4d 100644
--- a/isar/Example-Tokens.thy
+++ b/isar/Example-Tokens.thy
@@ -12,7 +12,7 @@ text {* Proper proof text -- \<^bitalic>naive version\<^eitalic>. *}
 
 theorem and_comms: "\<phi> \<and> \<psi> \<longrightarrow> \<psi> \<and> \<phi>"
 proof
-   assume "\<phi> \<and> \<psi>"
+  assume "\<phi> \<and> \<psi>"
   then show "\<psi> \<and> \<phi>"
   proof
     assume \<psi> and \<phi>
@@ -22,7 +22,7 @@ qed
 
 text {* \<^bbold>Unstructured\<^ebold> proof script. *}
 
-theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> (\<phi>\<^isub>\<beta>  ∧  \<phi>\<^isub>\<alpha>)"
+theorem "\<phi>\<^isub>\<alpha> \<and> \<phi>\<^isub>\<beta> \<longrightarrow> \<phi>\<^isub>\<beta> \<and> \<phi>\<^isub>\<alpha>"
   apply (rule impI)
   apply (erule conjE)
   apply (rule conjI)
-- 
cgit v1.2.3