Wed, 24 Apr 2013 16:43:19 +0200 | traytel | optimized proofs | changeset | files |
Wed, 24 Apr 2013 16:21:23 +0200 | blanchet | apply arguments to f and g in "case_cong" | changeset | files |
Wed, 24 Apr 2013 15:42:00 +0200 | blanchet | derive "map_cong" | changeset | files |
Wed, 24 Apr 2013 14:15:01 +0200 | blanchet | renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong" | changeset | files |
Wed, 24 Apr 2013 14:14:36 +0200 | blanchet | killed dead code | changeset | files |
Wed, 24 Apr 2013 14:05:16 +0200 | blanchet | eta-contracted weak congruence rules (like in the old package) | changeset | files |
Wed, 24 Apr 2013 13:16:21 +0200 | blanchet | honor user-specified name for map function | changeset | files |
Wed, 24 Apr 2013 13:16:20 +0200 | blanchet | honor user-specified set function names | changeset | files |