Thu, 22 Dec 2005 00:29:17 +0100 | wenzelm | Transform mutual rule into projection. | changeset | files |
Thu, 22 Dec 2005 00:29:15 +0100 | wenzelm | added Provers/project_rule.ML | changeset | files |
Thu, 22 Dec 2005 00:29:14 +0100 | wenzelm | structure ProjectRule; | changeset | files |
Thu, 22 Dec 2005 00:29:12 +0100 | wenzelm | * induct: improved treatment of mutual goals and mutual rules; | changeset | files |
Thu, 22 Dec 2005 00:29:11 +0100 | wenzelm | updated auxiliary facts for induct method; | changeset | files |
Thu, 22 Dec 2005 00:29:10 +0100 | wenzelm | prop_tr': proper handling of aprop marked as bound; | changeset | files |
Thu, 22 Dec 2005 00:29:09 +0100 | wenzelm | consume: expand defs in prems of concls; | changeset | files |