diff options
Diffstat (limited to 'lego/example.l')
| -rw-r--r-- | lego/example.l | 7 |
1 files changed, 6 insertions, 1 deletions
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 |