From 6189e10da761f1d63135efa068cc428454e069f2 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Fri, 24 Sep 1999 15:48:28 +0000
Subject: unified example with other proof assistants;

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

(limited to 'lego')

diff --git a/lego/example.l b/lego/example.l
index 4a506990..e5e6d7b8 100644
--- a/lego/example.l
+++ b/lego/example.l
@@ -6,9 +6,10 @@
 
 Module example 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;
-
-
+Goal {A,B:Prop}(and A B) -> (and B A);
+intros;
+Refine H;
+intros;
+andI;
+Immed;
+Save and_comms;
-- 
cgit v1.2.3