From 682b4c17840aaa694cf3c7684bb5b06bcb4108c2 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 15 Sep 2009 07:47:15 +0000
Subject: Fix compile errors

---
 isar/Example.thy | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index 720e5480..b0640146 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -9,10 +9,10 @@ theory Example imports Main begin
 
 text {* Proper proof text -- \textit{naive version}. *}
 
-theorem and_comms: "A & B --> B & A"
+theorem and_comms: "A \<and> B \<longrightarrow> B \<and> A"
 proof
-  assume "A & B"
-  then show "B & A"
+  assume "A \<and> B"
+  then show "B \<and> A"
   proof
     assume B and A
     then show ?thesis ..
@@ -22,6 +22,9 @@ qed
 text {* Unstructured proof script. *}
 
 theorem  "A & B --> B & A"
+by and_comms
+
+
   apply (rule impI)
   apply (erule conjE)
   apply (rule conjI)
-- 
cgit v1.2.3