1 files changed, 15 insertions, 0 deletions
diff --git a/lego/example.l b/lego/example.l
new file mode 100644
index 00000000..535d5712
--- /dev/null
+++ b/lego/example.l
@@ -0,0 +1,15 @@
+(*
+    Example proof script for Lego Proof General.
+ 
+    $Id$
+*)
+
+Module example Import lib_logic;
+
+Goal {A,B:Prop}(A /\ B) -> (B /\ A);
+intros;
+Refine H;
+intros;
+andI;
+Immed;
+Save and_comms;