src/HOL/Fun.thy
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
2010-12-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
2010-11-26 wenzelm 2010-11-26 keep private things private, without comments;
2010-11-23 hoelzl 2010-11-23 Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-11-18 haftmann 2010-11-18 map_fun combinator in theory Fun
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-08 nipkow 2010-09-08 put expand_(fun/set)_eq back in as synonyms, for compatibility
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-09-02 hoelzl 2010-09-02 Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
2010-09-02 hoelzl 2010-09-02 Introduce surj_on and replace surj and bij by abbreviations.
2010-09-02 hoelzl 2010-09-02 Permutation implies bij function
2010-09-02 hoelzl 2010-09-02 bij <--> bij_betw
2010-08-20 haftmann 2010-08-20 inj_comp and inj_fun
2010-07-12 haftmann 2010-07-12 dropped superfluous [code del]s
2010-07-09 haftmann 2010-07-09 nicer xsymbol syntax for fcomp and scomp
2010-04-16 wenzelm 2010-04-16 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-05 hoelzl 2010-03-05 generalized inj_uminus; added strict_mono_imp_inj_on
2010-03-04 hoelzl 2010-03-04 Rewrite rules for images of minus of intervals
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2009-12-30 krauss 2009-12-30 killed a few warnings
2009-12-21 haftmann 2009-12-21 merged
2009-12-21 haftmann 2009-12-21 moved lemmas o_eq_dest, o_eq_elim here
2009-12-18 huffman 2009-12-18 add lemma swap_triple
2009-12-16 huffman 2009-12-16 declare swap_self [simp], add lemma comp_swap
2009-10-29 haftmann 2009-10-29 moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
2009-10-22 nipkow 2009-10-22 inv_onto -> inv_into
2009-10-20 paulson 2009-10-20 Some new lemmas concerning sets
2009-10-19 berghofe 2009-10-19 Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
2009-10-18 nipkow 2009-10-18 Inv -> inv_onto, inv abbr. inv_onto UNIV.
2009-10-17 nipkow 2009-10-17 added the_inv_onto
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-10 haftmann 2009-09-10 early bootstrap of generic transfer procedure