From 2cffd85bad42fa08bd943646e02dbfa1a5bb0580 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 22 Jun 2000 15:55:35 +0000
Subject: Added missing proof.

---
 isa/Example.ML | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
index 1fec5c08..49b6ee5a 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -13,5 +13,7 @@ Goal "A & B --> B & A";
 qed "and_comms";
 
 Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)";
+by (blast_tac (claset()) 1);
+
 
 
-- 
cgit v1.2.3