aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
diff options
context:
space:
mode:
Diffstat (limited to 'lego')
-rw-r--r--lego/example.l6
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);