| Thu, 16 Oct 2008 22:44:29 +0200 | wenzelm | Drule.norm_hhf_eqs; | changeset | files |
| Thu, 16 Oct 2008 22:44:28 +0200 | wenzelm | prove_common: include all sorts from context into statement, check shyps of result; | changeset | files |
| Thu, 16 Oct 2008 22:44:27 +0200 | wenzelm | added rules for sort_constraint, include in norm_hhf_eqs; | changeset | files |
| Thu, 16 Oct 2008 22:44:26 +0200 | wenzelm | tuned; | changeset | files |
| Thu, 16 Oct 2008 22:44:25 +0200 | wenzelm | avoid accidental dependency of automated proof on sort equiv; | changeset | files |
| Thu, 16 Oct 2008 22:44:24 +0200 | wenzelm | explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts; | changeset | files |