src/HOL/Fun.thy
Thu, 18 Aug 2011 13:25:17 +0200 haftmann moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
Wed, 27 Jul 2011 19:34:30 +0200 hoelzl finite vimage on arbitrary domains
Sun, 17 Jul 2011 22:25:14 +0200 haftmann more on complement
Thu, 07 Jul 2011 21:53:53 +0200 nipkow added translation to fix critical pair between abbreviations for surj and ~=
Fri, 20 May 2011 21:38:32 +0200 hoelzl add surj_vimage_empty
Tue, 05 Apr 2011 11:44:34 +0200 blanchet added "no_atp" to Cantor's paradox
Fri, 21 Jan 2011 09:44:12 +0100 haftmann moved theorem
Tue, 11 Jan 2011 14:12:37 +0100 haftmann "enriched_type" replaces less specific "type_lifting"
Fri, 17 Dec 2010 17:43:54 +0100 wenzelm replaced command 'nonterminals' by slightly modernized version 'nonterminal';
Mon, 06 Dec 2010 09:25:05 +0100 haftmann moved bootstrap of type_lifting to Fun
Mon, 06 Dec 2010 09:19:10 +0100 haftmann replace `type_mapper` by the more adequate `type_lifting`
Fri, 26 Nov 2010 21:09:36 +0100 wenzelm keep private things private, without comments;
Tue, 23 Nov 2010 14:14:17 +0100 hoelzl Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
Thu, 18 Nov 2010 17:01:15 +0100 haftmann map_fun combinator in theory Fun
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
less more (0) -100 -60 tip