| Thu, 22 Dec 2005 00:28:43 +0100 | wenzelm | tuned induct proofs; | changeset | files |
| Thu, 22 Dec 2005 00:28:41 +0100 | wenzelm | mutual induct with *.inducts; | changeset | files |
| Thu, 22 Dec 2005 00:28:39 +0100 | wenzelm | wf_induct_rule: consumes 1; | changeset | files |