src/HOL/Fun.thy
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
2008-03-19 wenzelm 2008-03-19 more antiquotations;
2008-02-26 haftmann 2008-02-26 moved some set lemmas to Set.thy
2008-02-21 nipkow 2008-02-21 moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some
2008-01-10 berghofe 2008-01-10 Added test data generator for function type (from Pure/codegen.ML).
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp
2007-07-28 wenzelm 2007-07-28 simproc_setup fun_upd2;
2007-07-20 haftmann 2007-07-20 simplified HOL bootstrap
2007-07-11 berghofe 2007-07-11 Added ML bindings for sup_fun_eq and sup_bool_eq.
2007-05-09 haftmann 2007-05-09 moved recfun_codegen.ML to Code_Generator.thy
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-04-04 wenzelm 2007-04-04 ML antiquotes;
2007-03-16 haftmann 2007-03-16 moved lattice instance here
2006-12-27 haftmann 2006-12-27 explizit serialization for Haskell id
2006-12-18 haftmann 2006-12-18 infix syntax for generated code for composition
2006-11-27 haftmann 2006-11-27 moved order arities for fun and bool to Fun/Orderings
2006-11-13 haftmann 2006-11-13 dropped Typedef dependency
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-07-08 wenzelm 2006-07-08 simprocs: no theory argument -- use simpset context instead;
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-05-02 wenzelm 2006-05-02 replaced syntax/translations by abbreviation;