src/HOL/Fun.thy
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;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-03-23 nipkow 2006-03-23 Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
2005-11-11 huffman 2005-11-11 add header
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-17 wenzelm 2005-10-17 Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-08-01 wenzelm 2005-08-01 simprocs: Simplifier.inherit_bounds;
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-04-10 nipkow 2005-04-10 _(_|_) is now override_on
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-09 paulson 2005-02-09 new foldSet proofs
2005-01-14 nipkow 2005-01-14 made diff_less a simp rule
2004-11-21 nipkow 2004-11-21 added lemmas
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-08-04 nipkow 2004-08-04 added some inj_on thms
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2003-04-14 nipkow 2003-04-14 Added thms
2002-10-10 berghofe 2002-10-10 - Added range_ex1_eq - Removed obsolete theorems inj_o and inj_fun_lemma
2002-09-26 paulson 2002-09-26 Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
2001-12-11 wenzelm 2001-12-11 oops;
2001-12-10 wenzelm 2001-12-10 bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-21 wenzelm 2001-11-21 got rid of theory Inverse_Image;
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;