From eb8ad8d10763bc31b67bfc1f3c4bc3404b02a749 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 May 2001 17:58:06 +0000
Subject: Remove extra proof."

---
 isa/Example.ML | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
index 4795d79f..c607390f 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -12,6 +12,3 @@ Goal "A & B --> B & A";
   by (assume_tac 1);
 qed "and_comms";
 
-Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)";
-  by (blast_tac (claset()) 1);
-qed "";
-- 
cgit v1.2.3