src/HOL/Fun.thy
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Wed, 08 Sep 2010 10:45:55 +0200 nipkow put expand_(fun/set)_eq back in as synonyms, for compatibility
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Thu, 02 Sep 2010 21:08:31 +0200 hoelzl Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
Thu, 02 Sep 2010 11:54:09 +0200 hoelzl Introduce surj_on and replace surj and bij by abbreviations.
Thu, 02 Sep 2010 10:45:51 +0200 hoelzl Permutation implies bij function
Thu, 02 Sep 2010 10:36:45 +0200 hoelzl bij <--> bij_betw
Fri, 20 Aug 2010 17:46:55 +0200 haftmann inj_comp and inj_fun
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Fri, 09 Jul 2010 08:11:10 +0200 haftmann nicer xsymbol syntax for fcomp and scomp
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Fri, 05 Mar 2010 17:49:10 +0100 hoelzl generalized inj_uminus; added strict_mono_imp_inj_on
Thu, 04 Mar 2010 19:43:51 +0100 hoelzl Rewrite rules for images of minus of intervals
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Thu, 11 Feb 2010 23:00:22 +0100 wenzelm modernized translations;
Wed, 30 Dec 2009 10:24:53 +0100 krauss killed a few warnings
Mon, 21 Dec 2009 08:32:22 +0100 haftmann merged
Mon, 21 Dec 2009 08:32:03 +0100 haftmann moved lemmas o_eq_dest, o_eq_elim here
Fri, 18 Dec 2009 18:48:27 -0800 huffman add lemma swap_triple
Wed, 16 Dec 2009 14:38:35 -0800 huffman declare swap_self [simp], add lemma comp_swap
Thu, 29 Oct 2009 11:41:36 +0100 haftmann moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
Thu, 22 Oct 2009 09:27:48 +0200 nipkow inv_onto -> inv_into
Tue, 20 Oct 2009 16:32:51 +0100 paulson Some new lemmas concerning sets
Mon, 19 Oct 2009 16:43:45 +0200 berghofe Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
Sun, 18 Oct 2009 12:07:25 +0200 nipkow Inv -> inv_onto, inv abbr. inv_onto UNIV.
Sat, 17 Oct 2009 13:46:39 +0200 nipkow added the_inv_onto
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 10 Sep 2009 15:23:07 +0200 haftmann early bootstrap of generic transfer procedure
Mon, 10 Aug 2009 17:00:41 +0200 nipkow new lemma bij_comp
Wed, 22 Jul 2009 18:02:10 +0200 haftmann moved complete_lattice &c. into separate theory
Mon, 06 Jul 2009 14:19:13 +0200 haftmann moved Inductive.myinv to Fun.inv; tuned
Tue, 23 Jun 2009 12:09:30 +0200 haftmann uniformly capitialized names for subdirectories
Wed, 10 Jun 2009 15:04:33 +0200 haftmann separate directory for datatype package
Thu, 04 Jun 2009 13:26:32 +0200 nipkow A few finite lemmas
Tue, 19 May 2009 13:57:31 +0200 haftmann pretty printing of functional combinators for evaluation code
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Thu, 05 Mar 2009 08:23:08 +0100 haftmann dropped Id
Fri, 31 Oct 2008 10:35:30 +0100 berghofe Replaced arbitrary by undefined.
Fri, 10 Oct 2008 06:45:53 +0200 haftmann `code func` now just `code`
Mon, 23 Jun 2008 23:45:39 +0200 wenzelm Logic.all/mk_equals/mk_implies;
Fri, 13 Jun 2008 15:22:07 +0200 nipkow hide -> hide (open)
Thu, 12 Jun 2008 14:10:41 +0200 nipkow Hid swap
Tue, 10 Jun 2008 19:15:18 +0200 wenzelm tuned proofs -- case_tac *is* available here;
Tue, 10 Jun 2008 15:30:56 +0200 haftmann removed some dubious code lemmas
Wed, 09 Apr 2008 08:10:11 +0200 haftmann removed syntax from monad combinators; renamed mbind to scomp
Thu, 20 Mar 2008 12:04:53 +0100 haftmann added forward composition
Wed, 19 Mar 2008 22:50:42 +0100 wenzelm more antiquotations;
Tue, 26 Feb 2008 20:38:12 +0100 haftmann moved some set lemmas to Set.thy
Thu, 21 Feb 2008 17:33:58 +0100 nipkow moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
Thu, 10 Jan 2008 19:10:08 +0100 berghofe Added test data generator for function type (from Pure/codegen.ML).
Wed, 15 Aug 2007 12:52:56 +0200 paulson ATP blacklisting is now in theory data, attribute noatp
Sat, 28 Jul 2007 20:40:19 +0200 wenzelm simproc_setup fun_upd2;
Fri, 20 Jul 2007 14:27:56 +0200 haftmann simplified HOL bootstrap
Wed, 11 Jul 2007 11:02:07 +0200 berghofe Added ML bindings for sup_fun_eq and sup_bool_eq.
Wed, 09 May 2007 07:53:06 +0200 haftmann moved recfun_codegen.ML to Code_Generator.thy
Sun, 06 May 2007 21:50:17 +0200 haftmann changed code generator invocation syntax
Fri, 20 Apr 2007 11:21:42 +0200 haftmann Isar definitions are now added explicitly to code theorem table
Wed, 04 Apr 2007 00:10:59 +0200 wenzelm ML antiquotes;
Fri, 16 Mar 2007 21:32:09 +0100 haftmann moved lattice instance here
Wed, 27 Dec 2006 19:09:55 +0100 haftmann explizit serialization for Haskell id
less more (0) -100 -60 tip