| 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 |
| Fri, 23 Dec 2005 15:16:48 +0100 | wenzelm | added mk_conjunction_list2; | changeset | files |
| Fri, 23 Dec 2005 15:16:46 +0100 | wenzelm | conj_elim_precise: proper treatment of nested conjunctions; | changeset | files |
| Fri, 23 Dec 2005 15:16:46 +0100 | wenzelm | Thm.compose_no_flatten; | changeset | files |