Cleaned up example files so all demonstrate same theorem "conj_comms".

Would be nice to add more theorems to compare scripts in different
systems.

1 files changed, 6 insertions, 0 deletions

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);