Ticket #757 (new feature)
Opened 3 weeks ago
More sophisticated theorem orderings à la VSE
| Reported by: | till | Owned by: | maeder |
|---|---|---|---|
| Priority: | major | Milestone: | 0.95 |
| Component: | hets | Version: | 0.93 |
| Keywords: | Cc: |
Description
In a local node, allow the postulation or generation of orderings that guarantee correctness. Then, lesser theorems can be used in proofs even if they are not proved yet.
Note: See
TracTickets for help on using
tickets.
