From 93aff45f52f9bf14f64e5b42ef16aa24d15bd79a Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 15 Sep 2009 07:48:10 +0000
Subject: Revert accidental commit

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

(limited to 'isar/Example.thy')

diff --git a/isar/Example.thy b/isar/Example.thy
index b0640146..720e5480 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 \<and> B \<longrightarrow> B \<and> A"
+theorem and_comms: "A & B --> B & A"
 proof
-  assume "A \<and> B"
-  then show "B \<and> A"
+  assume "A & B"
+  then show "B & A"
   proof
     assume B and A
     then show ?thesis ..
@@ -22,9 +22,6 @@ 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