src/HOL/Fun.thy
2015-12-28 wenzelm 2015-12-28 former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-18 paulson 2015-11-18 New theorems mostly from Peter Gammie
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-10-27 paulson 2015-10-27 Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-09-21 paulson 2015-09-21 new lemmas and movement of lemmas into place
2015-08-13 haftmann 2015-08-13 more lemmas
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-02-11 Andreas Lochbihler 2015-02-11 add lemmas about bind and image
2015-02-11 paulson 2015-02-11 Merge
2015-02-10 paulson 2015-02-10 New lemmas and a bit of tidying up.
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-09-06 haftmann 2014-09-06 added various facts
2014-09-01 blanchet 2014-09-01 tuned structure inclusion
2014-06-21 ballarin 2014-06-21 Two basic lemmas on bij_betw.
2014-04-16 haftmann 2014-04-16 more simp rules for Fun.swap
2014-03-15 haftmann 2014-03-15 more complete set of lemmas wrt. image and composition
2014-03-13 haftmann 2014-03-13 tuned proofs
2014-03-09 haftmann 2014-03-09 bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned
2014-03-07 wenzelm 2014-03-07 more antiquotations;
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)
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-20 blanchet 2014-01-20 tuning
2014-01-16 blanchet 2014-01-16 moved lemmas from 'Fun_More_FP' to where they belong
2013-11-25 traytel 2013-11-25 eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-26 Andreas Lochbihler 2013-09-26 add lemmas
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-03 haftmann 2013-04-03 generalized lemma fold_image thanks to Peter Lammich
2012-10-18 haftmann 2012-10-18 simp results for simplification results of Inf/Sup expressions on bool; tuned proofs
2012-10-08 haftmann 2012-10-08 consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-04-19 huffman 2012-04-19 tuned lemmas (v)image_id; removed duplicate of vimage_id
2012-04-15 haftmann 2012-04-15 centralized enriched_type declaration, thanks to in-situ available Isar commands
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-02-22 bulwahn 2012-02-22 generalizing inj_on_Int
2012-02-05 bulwahn 2012-02-05 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 2012-02-05 adding a remark about lemma which is too special and should be removed
2011-11-20 wenzelm 2011-11-20 explicit is better than implicit;
2011-10-19 bulwahn 2011-10-19 removing old code generator setup for function types
2011-09-14 hoelzl 2011-09-14 renamed Complete_Lattices lemmas, removed legacy names
2011-09-13 huffman 2011-09-13 tuned proofs
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-10 haftmann 2011-09-10 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
2011-09-06 nipkow 2011-09-06 added new lemmas
2011-08-18 haftmann 2011-08-18 moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
2011-07-27 hoelzl 2011-07-27 finite vimage on arbitrary domains
2011-07-17 haftmann 2011-07-17 more on complement
2011-07-07 nipkow 2011-07-07 added translation to fix critical pair between abbreviations for surj and ~=
2011-05-20 hoelzl 2011-05-20 add surj_vimage_empty
2011-04-05 blanchet 2011-04-05 added "no_atp" to Cantor's paradox
2011-01-21 haftmann 2011-01-21 moved theorem
2011-01-11 haftmann 2011-01-11 "enriched_type" replaces less specific "type_lifting"
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-06 haftmann 2010-12-06 moved bootstrap of type_lifting to Fun