1 files changed, 7 insertions, 6 deletions
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;