| Thu, 22 Dec 2005 00:28:58 +0100 | wenzelm | mk_conjunction: proper treatment of bounds; | changeset | files |
| Thu, 22 Dec 2005 00:28:54 +0100 | wenzelm | fixed has_internal; | changeset | files |
| Thu, 22 Dec 2005 00:28:53 +0100 | wenzelm | Tactic.precise_conjunction_tac; | changeset | files |
| Thu, 22 Dec 2005 00:28:52 +0100 | wenzelm | added locale meta_conjunction_syntax and various conjunction rules; | changeset | files |
| Thu, 22 Dec 2005 00:28:51 +0100 | wenzelm | simplified setup: removed dest_concls, local_impI, conjI; | changeset | files |
| Thu, 22 Dec 2005 00:28:49 +0100 | wenzelm | induct_rulify; | changeset | files |
| Thu, 22 Dec 2005 00:28:47 +0100 | wenzelm | actually produce projected rules; | changeset | files |
| Thu, 22 Dec 2005 00:28:46 +0100 | wenzelm | *.inducts holds all projected rules; | changeset | files |
| Thu, 22 Dec 2005 00:28:44 +0100 | wenzelm | tuned; | changeset | files |
| 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 |
| Thu, 22 Dec 2005 00:28:36 +0100 | wenzelm | structure ProjectRule; | changeset | files |
| Thu, 22 Dec 2005 00:28:34 +0100 | wenzelm | updated auxiliary facts for induct method; | changeset | files |
| Wed, 21 Dec 2005 17:00:57 +0100 | haftmann | slight improvements | changeset | files |