| Thu, 16 Oct 2008 22:45:08 +0200 | wenzelm | goal-directed proof now enforces strict proof irrelevance wrt. sort hypotheses; | changeset | files |
| Thu, 16 Oct 2008 22:44:37 +0200 | wenzelm | added translations for SORT_CONSTRAINT | changeset | files |
| Thu, 16 Oct 2008 22:44:36 +0200 | wenzelm | conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result; | changeset | files |