diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-16 23:11:42 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-16 23:11:42 +0000 |
| commit | 0f4feea9ca0163946b2a971657b8e71c2931044d (patch) | |
| tree | 8507aa084284960e2443c7ac693b8e524abb7d9f /etc/lego | |
| parent | 4dfaa3700086d0cb6c9d8518dac894e58fa7f7a9 (diff) | |
Refactor several variable names; clean up, doc subterm markup and output display.
Diffstat (limited to 'etc/lego')
| -rw-r--r-- | etc/lego/pbp.l | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/etc/lego/pbp.l b/etc/lego/pbp.l index 82318dce..66a6df72 100644 --- a/etc/lego/pbp.l +++ b/etc/lego/pbp.l @@ -2,12 +2,14 @@ (* All using middle-clicks. - 1. Click on -> (Intros A B) - 2. Click on -> again (Intros H; Try Refine H) - 3. Click on A (Intros H1; Try Refine H1) - 4. Click on B (Intros H2; Try Refine H2) - 5. Click on A in A/\B (Refine pair; Try Assumption) - 6. Click on final B (Try Assumption) + 1. Click on -> (Pbp 0 3 1: Intros A B) + 2. Click on left (A/\B) (Pbp 1 2 1: Intros H; Try Refine H) + 3. Click on A (Pbp 4 2 1: Intros H1; Try Refine H1) + 4. Click on B (Pbp 5 2 1: Intros H2; Try Refine H2) + 5. Click on A in A/\B (Pbp 6 2 1: Refine pair; Try Assumption) + 6. Click on final B (Pbp 10: Try Assumption) + OR: + Click on assumption B (PbpHyp H2: Try Refine H2) QED!! *) |