src/HOL/Library/Countable.thy
Thu, 06 Sep 2012 08:59:50 -0700 huffman countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
Thu, 12 Apr 2012 18:39:19 +0200 wenzelm more standard method setup;
Sat, 17 Mar 2012 17:58:40 +0100 wenzelm more antiquotations;
Wed, 27 Jul 2011 19:35:00 +0200 hoelzl to_nat is injective on arbitrary domains
Thu, 23 Jun 2011 10:07:16 -0700 huffman add countable_datatype method for proving countable class instances
Mon, 22 Nov 2010 10:34:33 +0100 hoelzl Replace surj by abbreviation; remove surj_on.
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
Thu, 09 Sep 2010 14:38:14 +0200 bulwahn changing String.literal to a type instead of a datatype
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Mon, 05 Jul 2010 15:12:20 +0200 haftmann tuned proof
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Wed, 30 Jun 2010 16:28:13 +0200 haftmann added literal and typerep instances
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Wed, 10 Mar 2010 14:57:13 -0800 huffman new theory Library/Nat_Bijection.thy
Fri, 26 Feb 2010 09:20:18 +0100 haftmann adjusted to cs. e4a7947e02b8
Thu, 12 Nov 2009 17:21:51 +0100 hoelzl Remove map_compose, replaced by map_map
Sun, 12 Jul 2009 10:14:51 +0200 nipkow More about gcd/lcm, and some cleaning up
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Sat, 14 Feb 2009 11:10:35 -0800 huffman add lemma surj_from_nat
Thu, 12 Feb 2009 11:04:22 -0800 huffman move countability proof from Rational to Countable; add instance rat :: countable
Tue, 03 Feb 2009 21:26:21 +0100 haftmann handling type classes without parameters
Fri, 16 Jan 2009 14:58:56 +0100 haftmann migrated class package to new locale implementation
Mon, 17 Nov 2008 17:00:55 +0100 haftmann tuned unfold_locales invocation
Mon, 07 Jul 2008 08:47:17 +0200 haftmann absolute imports of HOL/*.thy theories
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Wed, 09 Apr 2008 05:31:04 +0200 huffman fix spelling
Tue, 08 Apr 2008 18:30:40 +0200 krauss Generic conversion and tactic "atomize_elim" to convert elimination rules
Thu, 20 Mar 2008 12:01:12 +0100 haftmann adjusted authorship
Mon, 10 Mar 2008 18:44:20 +0100 huffman instance fun :: (finite, countable) countable
Wed, 27 Feb 2008 21:41:07 +0100 haftmann added theory for countable types
less more (0) tip