src/HOL/Quotient_Examples/Lift_FSet.thy
2013-08-13 kuncar 2013-08-13 remove unnecessary dependencies on Library/Quotient_*
2013-06-08 huffman 2013-06-08 implement 'transferred' attribute for transfer package, with support for monotonicity of !!/==>
2013-05-15 kuncar 2013-05-15 stronger reflexivity prover
2013-03-13 kuncar 2013-03-13 rename fset_member to fmember and prove parametricity
2013-03-13 traytel 2013-03-13 BNF uses fset defined via Lifting/Transfer rather than Quotient
2013-03-08 kuncar 2013-03-08 simplify Lift_FSet because we have parametricity in Lifting now
2012-11-26 kuncar 2012-11-26 generate a parameterized correspondence relation
2012-05-16 kuncar 2012-05-16 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
2012-04-22 huffman 2012-04-22 adapt to changes in generated transfer rules (cf. 4483c004499a)
2012-04-22 huffman 2012-04-22 new example theory for quotient/transfer