src/HOL/Library/Quotient_Set.thy
Thu, 06 Mar 2014 15:40:33 +0100 blanchet renamed 'fun_rel' to 'rel_fun'
Thu, 06 Mar 2014 15:10:56 +0100 blanchet renamed 'vset_rel' to 'rel_vset'
Tue, 13 Aug 2013 15:59:22 +0200 kuncar move Lifting/Transfer relevant parts of Library/Quotient_* to Main
Mon, 10 Jun 2013 06:08:14 -0700 huffman more transfer rules for sets
Wed, 15 May 2013 12:10:39 +0200 kuncar stronger reflexivity prover
Mon, 13 May 2013 13:59:04 +0200 kuncar better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
Fri, 08 Mar 2013 13:21:52 +0100 kuncar add [relator_mono] and [relator_distr] rules
Thu, 24 May 2012 14:20:23 +0200 kuncar prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
Wed, 16 May 2012 19:15:45 +0200 kuncar infrastructure that makes possible to prove that a relation is reflexive
Mon, 14 May 2012 17:09:11 +0200 huffman add transfer rule for set_rel
Thu, 26 Apr 2012 12:01:58 +0200 kuncar use a quot_map theorem attribute instead of the complicated map attribute
Sun, 22 Apr 2012 20:16:30 +0200 huffman add transfer rule for set difference
Sun, 22 Apr 2012 11:05:04 +0200 huffman new example theory for quotient/transfer
Sat, 21 Apr 2012 13:12:27 +0200 huffman move alternative definition lemmas into Lifting.thy;
Sat, 21 Apr 2012 11:02:01 +0200 huffman added covariant relator set_rel, with transfer rules for set operations
less more (0) -15 tip