| Thu, 24 May 2012 14:20:23 +0200 | kuncar | prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule | file | diff | annotate |
| Mon, 21 May 2012 16:36:48 +0200 | kuncar | quot_del attribute, it allows us to deregister quotient types | file | diff | annotate |
| Wed, 16 May 2012 19:15:45 +0200 | kuncar | infrastructure that makes possible to prove that a relation is reflexive | file | diff | annotate |
| Thu, 26 Apr 2012 21:58:16 +0200 | kuncar | added a basic sanity check for quot_map | file | diff | annotate |
| Thu, 26 Apr 2012 12:01:58 +0200 | kuncar | use a quot_map theorem attribute instead of the complicated map attribute | file | diff | annotate |
| Fri, 20 Apr 2012 18:29:21 +0200 | kuncar | hide the invariant constant for relators: invariant_commute infrastracture | file | diff | annotate |
| Tue, 03 Apr 2012 16:26:48 +0200 | kuncar | new package Lifting - initial commit | file | diff | annotate |