| Sat, 14 Jun 2008 23:20:12 +0200 | wenzelm | export subgoal_tac, subgoals_tac, thin_tac; | changeset | files |
| Sat, 14 Jun 2008 23:20:11 +0200 | wenzelm | prove: full Variable.declare_term, including constraints; | changeset | files |
| Sat, 14 Jun 2008 23:20:10 +0200 | wenzelm | prove_standard: more precises argument passing; | changeset | files |
| Sat, 14 Jun 2008 23:20:09 +0200 | wenzelm | InductTacs.case_tac: removed obsolete declare, which is now part of Goal.prove; | changeset | files |
| Sat, 14 Jun 2008 23:20:07 +0200 | wenzelm | simplified InductTacs.case_tac/induct_tac; | changeset | files |
| Sat, 14 Jun 2008 23:20:06 +0200 | wenzelm | tuned proof; | changeset | files |
| Sat, 14 Jun 2008 23:20:05 +0200 | wenzelm | removed obsolete nat_induct_tac -- cannot work without; | changeset | files |