From 0606a0391305da5a3a87bebcef15d3cf2a66be6c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 13 Sep 1999 14:03:38 +0000
Subject: Cleaned up example files so all demonstrate same theorem
 "conj_comms". Would be nice to add more theorems to compare scripts in
 different systems.

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

(limited to 'isa/example.ML')

diff --git a/isa/example.ML b/isa/example.ML
index 8ea12dfd..41ea20be 100644
--- a/isa/example.ML
+++ b/isa/example.ML
@@ -1,10 +1,7 @@
 (*
-    Example proof script for Isabelle
-
-    David Aspinall <da@dcs.ed.ac.uk>
+    Example proof script for Isabelle Proof General.
 
     $Id$
-
 *)    
 
 Goal "(A & B)-->(B & A)";
-- 
cgit v1.2.3