spechub/Hets — pull request #1434 by eugenk (2014-12-27 11:00:34+00:00)
Title: Allow selection of axioms.

This shall fix #1424. It adds the prove option `axioms`. `axioms` expects a comma separated list of axiom names which are supposed to be used in the proof attempt (white list).

To try this, simply start the hets server and call
```
http://localhost:8000/prove/file%3A%2F%2F%2Fprivate%2Ftmp%2FGroups.casl?node=Group;axioms=Ax2,leftunit,ga_assoc___%2B__
http://localhost:8000/prove/file%3A%2F%2F%2Fprivate%2Ftmp%2FGroups.casl?node=Group;axioms=Ax2,leftunit
```
in your browser while having the following /tmp/Group.casl:
```
library Examples/Groups

spec Group =
sort s
ops 0:s;
-__ :s->s; %(inverse)%
__+__ :s*s->s, assoc
forall x,y:s
. x+(-x) = 0
. x+0=x %(leftunit)%
. 0+x=x %(rightunit)% %implied
end
```

In another pull request (WIP) the options are expected as POST parameters because (a) the list of axioms can be very long and (b) using GET for a proof creation is not compliant to a RESTful API.