src/HOL/Fun.thy
2016-08-02 wenzelm tuned proof;
2016-08-02 wenzelm misc tuning and modernization;
2016-08-01 wenzelm misc tuning and modernization;
2016-07-29 Andreas Lochbihler add lemmas contributed by Peter Gammie
2016-07-08 haftmann avoid to hide equality behind (output) abbreviation
2016-07-05 wenzelm misc tuning and modernization;
2016-07-02 haftmann more theorems
2016-06-20 wenzelm prefer HOL definitions;
2016-06-20 wenzelm tuned proof;
2016-06-20 wenzelm misc tuning and modernization;
2016-05-09 paulson renamings and refinements
2016-04-04 paulson Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
2016-03-14 paulson Refactoring (moving theorems into better locations), plus a bit of new material
2016-02-23 nipkow more canonical names
2015-12-28 wenzelm former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-07 wenzelm isabelle update_cartouches -c -t;
2015-11-18 paulson New theorems mostly from Peter Gammie
2015-11-11 Andreas Lochbihler add various lemmas
2015-10-27 paulson Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-09 wenzelm discontinued specific HTML syntax;
2015-09-21 paulson new lemmas and movement of lemmas into place
2015-08-13 haftmann more lemmas
2015-07-18 wenzelm isabelle update_cartouches;
2015-05-26 paulson New material about paths, and some lemmas
2015-02-11 Andreas Lochbihler add lemmas about bind and image
2015-02-11 paulson Merge
2015-02-10 paulson New lemmas and a bit of tidying up.
2015-02-10 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
2014-11-02 wenzelm modernized header uniformly as section;
2014-10-30 wenzelm eliminated aliases;
2014-09-06 haftmann added various facts
2014-09-01 blanchet tuned structure inclusion
2014-06-21 ballarin Two basic lemmas on bij_betw.
2014-04-16 haftmann more simp rules for Fun.swap
2014-03-15 haftmann more complete set of lemmas wrt. image and composition
2014-03-13 haftmann tuned proofs
2014-03-09 haftmann bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
2014-03-07 wenzelm more antiquotations;
2014-02-14 blanchet renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
2014-02-12 blanchet renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-20 blanchet tuning
2014-01-16 blanchet moved lemmas from 'Fun_More_FP' to where they belong
2013-11-25 traytel eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
2013-10-18 blanchet killed most "no_atp", to make Sledgehammer more complete
2013-09-26 Andreas Lochbihler add lemmas
2013-06-23 haftmann migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-04-18 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
2013-04-03 haftmann generalized lemma fold_image thanks to Peter Lammich
2012-10-18 haftmann simp results for simplification results of Inf/Sup expressions on bool;
2012-10-08 haftmann consolidated names of theorems on composition;
2012-08-22 wenzelm prefer ML_file over old uses;
2012-04-19 huffman tuned lemmas (v)image_id;
2012-04-15 haftmann centralized enriched_type declaration, thanks to in-situ available Isar commands
2012-03-15 wenzelm declare command keywords via theory header, including strict checking outside Pure;
2012-02-22 bulwahn generalizing inj_on_Int
2012-02-05 bulwahn removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
2012-02-05 bulwahn adding a remark about lemma which is too special and should be removed
2011-11-20 wenzelm explicit is better than implicit;
2011-10-19 bulwahn removing old code generator setup for function types
2011-09-14 hoelzl renamed Complete_Lattices lemmas, removed legacy names
less more (0) -100 -60 tip