From 58b9e2ceeca8079d139ee1c0d8e5653ba69a403f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 9 May 2000 15:58:29 +0000
Subject: New goal.

---
 isa/Example.ML | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
index bf5ee3f0..673f7c6f 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -12,4 +12,6 @@ by (assume_tac 1);
 by (assume_tac 1);
 qed "and_comms";
 
-Goal "P(x) --> Q(x)";
+Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)";
+
+
-- 
cgit v1.2.3