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 |