| Thu, 24 May 2012 15:03:06 +0200 | kuncar | merged | changeset | files |
| Thu, 24 May 2012 14:20:25 +0200 | kuncar | drop the feature that more than one quotient type can be defined by quotient_type -> it causes problems | changeset | files |
| Thu, 24 May 2012 14:20:23 +0200 | kuncar | prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule | changeset | files |