| Fri, 26 Nov 2010 21:31:46 +0100 | wenzelm | explicit use of unprefix; | changeset | files |
| Fri, 26 Nov 2010 21:09:36 +0100 | wenzelm | keep private things private, without comments; | changeset | files |
| 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 |