| Tue, 30 Nov 2010 17:19:11 +0100 | haftmann | adaptions to changes in Equiv_Relation.thy | changeset | files |
| 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 |