search

data61 / PSL

Other
65 stars 9 forks source link

UR: proof states are not updated after proving new conjectures! #186

Open yutakang opened 3 years ago

yutakang commented 3 years ago

In the current implementation, proof states are not updated after proving new conjectures!

Therefore, subsequent proof attempts are unable to take advantage of such proved conjectures.

This needs to be fixed.

yutakang commented 3 years ago

Probably I can do something similar to what I did in Australia for Cogent.

yutakang commented 3 years ago

That is, use Local_Theory.note (a, ths).

yutakang commented 3 years ago

I have to use Proof.theorem to update Proof.state using Local_Theory.note as is done in this code.