| Tue, 30 Nov 2010 15:58:21 +0100 | haftmann | merged | changeset | files |
| Tue, 30 Nov 2010 15:58:09 +0100 | haftmann | more systematic and compact proofs on type relation operators using natural deduction rules | changeset | files |
| Tue, 30 Nov 2010 15:58:09 +0100 | haftmann | adapted proofs to slightly changed definitions of congruent(2) | changeset | files |
| Mon, 29 Nov 2010 22:47:55 +0100 | haftmann | reorienting iff in Quotient_rel prevents simplifier looping; | changeset | files |
| Mon, 29 Nov 2010 22:41:17 +0100 | haftmann | replaced slightly odd locale congruent2 by plain definition | changeset | files |
| 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 |