| Fri, 23 Dec 2005 15:21:05 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 23 Dec 2005 15:18:13 +0100 | wenzelm | * Provers/induct: support simultaneous goals with mutual rules; | changeset | files |
| Fri, 23 Dec 2005 15:16:58 +0100 | wenzelm | induct etc.: admit multiple rules; | changeset | files |
| Fri, 23 Dec 2005 15:16:56 +0100 | wenzelm | backpatching of Substring.full; | changeset | files |
| Fri, 23 Dec 2005 15:16:55 +0100 | wenzelm | goal/qed: proper treatment of two levels of conjunctions; | changeset | files |
| Fri, 23 Dec 2005 15:16:53 +0100 | wenzelm | Logic.mk_conjunction_list; | changeset | files |
| Fri, 23 Dec 2005 15:16:52 +0100 | wenzelm | turned bicompose_no_flatten into compose_no_flatten, without elimination; | changeset | files |
| Fri, 23 Dec 2005 15:16:49 +0100 | wenzelm | CONJUNCTS: full nesting (again), PRECISE_CONJUNCTS: outer level of nesting; | changeset | files |