src/HOL/Quotient_Examples/Lift_FSet.thy
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2014-11-10 traytel 2014-11-10 dropped redundant transfer rules (now proved and registered by datatype and plugins)
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-08-07 blanchet 2014-08-07 no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-02-25 kuncar 2014-02-25 simplify and repair proofs due to df0fda378813
2014-02-19 blanchet 2014-02-19 merged 'List.set' with BNF-generated 'set'
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