From cd6c2b24c5b81465d3dbcc292b4457ed37ab9fb1 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Fri, 6 Aug 1999 18:01:09 +0000
Subject: tuned;

---
 isa/example.ML | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'isa/example.ML')

diff --git a/isa/example.ML b/isa/example.ML
index a8922e87..8ea12dfd 100644
--- a/isa/example.ML
+++ b/isa/example.ML
@@ -7,8 +7,7 @@
 
 *)    
 
-goal HOL.thy
-  "(A & B)-->(B & A)";
+Goal "(A & B)-->(B & A)";
 br impI 1;
 br conjI 1;
 be conjE 1;
@@ -16,4 +15,3 @@ ba 1;
 be conjE 1;
 ba 1;
 qed "and_comms";
-
-- 
cgit v1.2.3