From 9080a41cf03b726ff9da2a3ac15e4c6155dd0749 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 8 Sep 1998 15:34:31 +0000
Subject: Example copied from texinfo manual

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

(limited to 'lego/example.l')

diff --git a/lego/example.l b/lego/example.l
index c82e7b2c..b7a952d1 100644
--- a/lego/example.l
+++ b/lego/example.l
@@ -1,2 +1,7 @@
+Module Walkthrough Import lib_logic;
+Goal and_commutes: {A,B:Prop}(and A B) -> (and B A);
+intros;andI;
+Refine H;intros;Immed;Refine H;intros; Immed;
+Save and_commutes;
+
 
-INSERT HANDY LEGO EXAMPLE HERE!
\ No newline at end of file
-- 
cgit v1.2.3