src/HOL/Library/Groups_Big_Fun.thy
15 months ago ballarin 2018-03-04 Drop rewrites after defines in interpretations.
20 months ago haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-07-11 wenzelm 2016-07-11 tuned;
2016-06-11 haftmann 2016-06-11 boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-02 haftmann 2015-12-02 modernized
2015-11-14 haftmann 2015-11-14 prefer "rewrites" and "defines" to note rewrite morphisms
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-24 haftmann 2014-09-24 added lemmas
2014-09-06 haftmann 2014-09-06 theory about sum and product on function bodies