From 0606a0391305da5a3a87bebcef15d3cf2a66be6c Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
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.

---
 lego/example.l | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'lego')

diff --git a/lego/example.l b/lego/example.l
index 52643424..4a506990 100644
--- a/lego/example.l
+++ b/lego/example.l
@@ -1,3 +1,9 @@
+(*
+    Example proof script for Lego Proof General.
+ 
+    $Id$
+*)
+
 Module example Import lib_logic;
 
 Goal and_commutes: {A,B:Prop}(and A B) -> (and B A);
-- 
cgit v1.2.3