From 8955ffee5e7b18241e1c13ab6228e64d2893f134 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 23 Mar 2005 17:26:24 +0000
Subject: Use another symbol

---
 isar/Example-Xsym.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/isar/Example-Xsym.thy b/isar/Example-Xsym.thy
index c731143b..48661f6a 100644
--- a/isar/Example-Xsym.thy
+++ b/isar/Example-Xsym.thy
@@ -24,7 +24,7 @@ text {* Proper proof text -- \textit{advanced version}. *}
 
 theorem "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
+  assume "A \<and> B"
   then obtain B and A ..
   then show "B \<and> A" ..
 qed
-- 
cgit v1.2.3

