src/HOL/Nat_Transfer.thy
22 months ago haftmann 2017-10-08 dropped dead code
2016-10-17 nipkow 2016-10-17 setprod -> prod
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-08-10 nipkow 2016-08-10 "split add" -> "split"
2016-02-17 haftmann 2016-02-17 dropped various legacy fact bindings
2015-11-13 paulson 2015-11-13 Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-06-28 haftmann 2014-06-28 fact consolidation
2013-02-28 wenzelm 2013-02-28 proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);
2012-12-07 wenzelm 2012-12-07 avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-03 huffman 2012-04-03 renamed Tools/transfer.ML to Tools/legacy_transfer.ML
2012-04-01 huffman 2012-04-01 removed Nat_Numeral.thy, moving all theorems elsewhere
2011-05-20 krauss 2011-05-20 clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton
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-03-18 haftmann 2010-03-18 meaningful transfer certificate
2010-03-09 haftmann 2010-03-09 misc tuning
2010-03-08 haftmann 2010-03-08 transfer: avoid camel case
2010-03-03 haftmann 2010-03-03 tuned whitespace
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-09-10 haftmann 2009-09-10 obey underscore naming convention