src/HOL/Quotient_Examples/Lift_FSet.thy
Mon, 26 Nov 2012 14:20:51 +0100 kuncar generate a parameterized correspondence relation
Wed, 16 May 2012 19:17:20 +0200 kuncar generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
Sun, 22 Apr 2012 17:54:47 +0200 huffman adapt to changes in generated transfer rules (cf. 4483c004499a)
Sun, 22 Apr 2012 11:05:04 +0200 huffman new example theory for quotient/transfer
less more (0) tip