Mon, 29 Nov 2010 22:32:06 +0100 | haftmann | replaced slightly odd locale congruent by plain definition | changeset | files |
Mon, 29 Nov 2010 13:44:54 +0100 | haftmann | equivI has replaced equiv.intro | changeset | files |
Mon, 29 Nov 2010 12:15:14 +0100 | haftmann | moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; | changeset | files |
Mon, 29 Nov 2010 12:14:46 +0100 | haftmann | moved generic definitions about relations from Quotient.thy to Predicate; | changeset | files |
Mon, 29 Nov 2010 12:14:43 +0100 | haftmann | moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations; | changeset | files |
Tue, 30 Nov 2010 08:58:47 -0800 | huffman | simplify proof of LIMSEQ_unique | changeset | files |