src/HOL/Quotient_Examples/Lift_DList.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2014-02-25 kuncar 2014-02-25 simplify and repair proofs due to df0fda378813
2014-02-18 kuncar 2014-02-18 simplify proofs because of the stronger reflexivity prover
2014-02-16 blanchet 2014-02-16 folded 'list_all2' with the relator generated by 'datatype_new'
2013-08-13 kuncar 2013-08-13 remove unnecessary dependencies on Library/Quotient_*
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-04-04 kuncar 2012-04-04 support non-open typedefs; define cr_rel in terms of a rep function for typedefs
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit