| Wed, 13 Jun 2007 00:01:41 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
| Mon, 11 Dec 2006 16:06:14 +0100 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
| Mon, 11 Sep 2006 21:35:19 +0200 | wenzelm | induct method: renamed 'fixing' to 'arbitrary'; | file | diff | annotate |
| Wed, 02 Aug 2006 23:09:49 +0200 | wenzelm | tuned proofs; | file | diff | annotate |
| Wed, 02 Aug 2006 22:27:08 +0200 | wenzelm | lemma da_good_approx: adapted induction (was exploting lifted obtain result); | file | diff | annotate |
| Mon, 12 Jun 2006 20:58:25 +0200 | wenzelm | avoid accidental binding of ?Jmp; | file | diff | annotate |