| 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 |
| Fri, 26 Nov 2010 12:03:18 +0100 | haftmann | globbing constant expressions use more idiomatic underscore rather than star | changeset | files |