src/HOL/Quotient_Examples/Lift_Fun.thy
2017-08-18 wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-03-06 blanchet 2014-03-06 renamed 'endofun_rel' to 'rel_endofun'
2014-02-14 blanchet 2014-02-14 renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2012-04-13 wenzelm 2012-04-13 updated headers;
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-03-26 kuncar 2012-03-26 tuned comment
2012-03-26 kuncar 2012-03-26 tuned proof - no smt call
2012-03-23 kuncar 2012-03-23 fix example files
2012-03-23 kuncar 2012-03-23 fix Quotient_Examples
2011-12-09 kuncar 2011-12-09 added an example file with lifting of constants with contravariant and co/contravariant types