src/HOL/Library/Quotient_Set.thy
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
less more (0) -10 -3 tip