spechub/Hets — pull request #1428 by eugenk (2014-12-11 20:26:31+00:00)
Title: Allow to pass `theorems` in prove-request

There already was a `theorems` command, which was not used in the
RESTful API. It can now be passed to select theorems to be proven. If
it is empty or omitted, all theorems in the node/theory will be proven.

This shall fix #1425. Other than stated in the issue, instead of the key `goals`, I chose the key `theorems` because the availability of that one was already implemented and it suits to the situation.

This does not yet accept the options via POST. This shall be done in a new issue.

To try this, simply start the hets server and call
```
http://localhost:8000/prove/file%3A%2F%2F%2Ftmp%2FGroups.casl?node=Group;theorems=zero_plus
```
in your browser while having the following `/tmp/Group.casl`:
```
spec Group =
sort s
ops 0:s;
-__ :s->s;
__+__ :s*s->s, assoc
forall x,y:s
. x+(-x) = 0
. x+0=x %(leftunit)%
. 0+x=x %(rightunit)% %implied
. 0+0=0 %(zero_plus)% %implied
end

spec Empty =
sort t
end
```