src/HOL/Quotient_Examples/Quotient_Int.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;
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-06-11 Thomas Sewell 2014-06-11 Hypsubst preserves equality hypotheses Fixes included for various theories affected by this change.
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-04-02 Christian Urban 2012-04-02 tuned proofs
2012-03-23 kuncar 2012-03-23 fix Quotient_Examples
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-01-08 wenzelm 2011-01-08 tuned headers;
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-12-03 krauss 2010-12-03 eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended
2010-11-09 haftmann 2010-11-09 fun_rel_def is no simp rule by default
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-06-29 Christian Urban 2010-06-29 cosmetics: avoided statement of raw theorems, used the method descending instead
2010-04-29 Cezary Kaliszyk 2010-04-29 Tuning the quotient examples