src/HOL/Fun.thy
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
2009-08-10 nipkow 2009-08-10 new lemma bij_comp
2009-07-22 haftmann 2009-07-22 moved complete_lattice &c. into separate theory
2009-07-06 haftmann 2009-07-06 moved Inductive.myinv to Fun.inv; tuned
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories
2009-06-10 haftmann 2009-06-10 separate directory for datatype package
2009-06-04 nipkow 2009-06-04 A few finite lemmas
2009-05-19 haftmann 2009-05-19 pretty printing of functional combinators for evaluation code
2009-05-09 nipkow 2009-05-09 lemmas by Andreas Lochbihler
2009-03-05 haftmann 2009-03-05 dropped Id
2008-10-31 berghofe 2008-10-31 Replaced arbitrary by undefined.
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-13 nipkow 2008-06-13 hide -> hide (open)
2008-06-12 nipkow 2008-06-12 Hid swap
2008-06-10 wenzelm 2008-06-10 tuned proofs -- case_tac *is* available here;
2008-06-10 haftmann 2008-06-10 removed some dubious code lemmas
2008-04-09 haftmann 2008-04-09 removed syntax from monad combinators; renamed mbind to scomp
2008-03-20 haftmann 2008-03-20 added forward composition