| Thu, 02 Oct 2008 12:17:20 +0200 | berghofe | Yet another proof of Newman's lemma, this time using the coherent logic prover. | changeset | files |
| Wed, 01 Oct 2008 22:33:29 +0200 | wenzelm | unit_source: more rigid parsing, stop after final qed; | changeset | files |
| Wed, 01 Oct 2008 22:33:28 +0200 | wenzelm | excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context; | changeset | files |
| Wed, 01 Oct 2008 22:33:24 +0200 | wenzelm | replaced can_defer by is_relevant (negation); | changeset | files |