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 \ B \ B \ A" proof - assume "A & B" + assume "A \ B" then obtain B and A .. then show "B \ A" .. qed -- cgit v1.2.3