Wed, 07 May 2008 10:59:23 +0200 | berghofe | Rephrased calculational proofs to avoid problems with HO unification | file | diff | annotate |
Wed, 11 Jul 2007 11:14:51 +0200 | berghofe | Adapted to new inductive definition package. | file | diff | annotate |
Wed, 13 Jun 2007 18:30:11 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
Wed, 07 Feb 2007 17:46:03 +0100 | berghofe | Adapted to changes in Finite_Set theory. | file | diff | annotate |
Wed, 23 Nov 2005 22:26:13 +0100 | wenzelm | tuned induction proofs; | file | diff | annotate |
Wed, 16 Nov 2005 17:50:35 +0100 | wenzelm | tuned; | file | diff | annotate |
Thu, 10 Nov 2005 21:14:05 +0100 | wenzelm | tuned proofs; | file | diff | annotate |