From 13cd8eac3946221fdb51d4cb6749eac2af82555b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 20 Oct 1998 10:31:58 +0000
Subject: Removed duplicate proof

---
 isa/example.ML | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'isa/example.ML')

diff --git a/isa/example.ML b/isa/example.ML
index 5a6f7dfb..a8922e87 100644
--- a/isa/example.ML
+++ b/isa/example.ML
@@ -17,12 +17,3 @@ be conjE 1;
 ba 1;
 qed "and_comms";
 
-goal HOL.thy
-  "(A & B)-->(B & A)";
-br impI 1;
-br conjI 1;
-be conjE 1;
-ba 1;
-be conjE 1;
-ba 1;
-qed "and_comms";
-- 
cgit v1.2.3