From f2e7d83e6c2a68cc07b27332fc9cc7ef07400869 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Wed, 2 Aug 2000 15:34:38 +0000
Subject: tuned;

---
 isa/Example.ML | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'isa/Example.ML')

diff --git a/isa/Example.ML b/isa/Example.ML
index 49b6ee5a..4795d79f 100644
--- a/isa/Example.ML
+++ b/isa/Example.ML
@@ -2,7 +2,7 @@
     Example proof script for Isabelle Proof General.
 
     $Id$
-*)    
+*)
 
 Goal "A & B --> B & A";
   by (rtac impI 1);
@@ -13,7 +13,5 @@ Goal "A & B --> B & A";
 qed "and_comms";
 
 Goal "(ALL x. P(x) --> Q) --> ((EX x. P(x)) --> Q)";
-by (blast_tac (claset()) 1);
-
-
-
+  by (blast_tac (claset()) 1);
+qed "";
-- 
cgit v1.2.3