diff options
| author | Healfdene Goguen | 1997-11-20 16:47:48 +0000 |
|---|---|---|
| committer | Healfdene Goguen | 1997-11-20 16:47:48 +0000 |
| commit | 1c8a7b0b87cb94c3d0fa23f3492ee03b00606032 (patch) | |
| tree | aa60be2621bd2cfc4d1f1158acfe006ec31bdef2 /todo | |
| parent | 41a87c513357da8bc0dce196c4ec46255826ba10 (diff) | |
Added proof-global-p to test whether a 'vanilla should be lifted above
active lemmas.
Separated proof-lift-global as separate command to lift global
declarations above active lemmas.
Fixed usual problem that 'cmd is nil for comments in this code.
Made lifting globals start from beginning of file rather than go
backwards.
Fixed bug in pbp code proof-shell-analyse-structure, where stack
wasn't cleared for new goal-hyp's.
Diffstat (limited to 'todo')
0 files changed, 0 insertions, 0 deletions