| Fri, 26 Nov 2010 20:52:21 +0100 | wenzelm | eliminated some clones of eq_list; | changeset | files |
| Fri, 26 Nov 2010 18:07:00 +0100 | nipkow | merged | changeset | files |
| Fri, 26 Nov 2010 18:06:48 +0100 | nipkow | new lemma | changeset | files |
| Fri, 26 Nov 2010 17:54:15 +0100 | wenzelm | lemma trans_sym allows single-step "normalization" in Isar, e.g. via moreover/ultimately; | changeset | files |
| Fri, 26 Nov 2010 16:28:34 +0100 | wenzelm | prefer non-classical eliminations in Pure reasoning, notably "rule" steps; | changeset | files |
| Fri, 26 Nov 2010 14:40:33 +0100 | wenzelm | discontinued global "Isabelle" symlink, to make each distribution even more self-contained; | changeset | files |
| Fri, 26 Nov 2010 14:19:16 +0100 | wenzelm | more correct spelling; | changeset | files |