src/HOL/Library/Countable.thy
2011-07-27 hoelzl 2011-07-27 to_nat is injective on arbitrary domains
2011-06-23 huffman 2011-06-23 add countable_datatype method for proving countable class instances
2010-11-22 hoelzl 2010-11-22 Replace surj by abbreviation; remove surj_on.
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-09 bulwahn 2010-09-09 changing String.literal to a type instead of a datatype
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-07-05 haftmann 2010-07-05 tuned proof
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-30 haftmann 2010-06-30 added literal and typerep instances
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-03-10 huffman 2010-03-10 new theory Library/Nat_Bijection.thy
2010-02-26 haftmann 2010-02-26 adjusted to cs. e4a7947e02b8
2009-11-12 hoelzl 2009-11-12 Remove map_compose, replaced by map_map
2009-07-12 nipkow 2009-07-12 More about gcd/lcm, and some cleaning up
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-02-14 huffman 2009-02-14 add lemma surj_from_nat
2009-02-12 huffman 2009-02-12 move countability proof from Rational to Countable; add instance rat :: countable
2009-02-03 haftmann 2009-02-03 handling type classes without parameters
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2008-11-17 haftmann 2008-11-17 tuned unfold_locales invocation
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2008-04-09 huffman 2008-04-09 fix spelling
2008-04-08 krauss 2008-04-08 Generic conversion and tactic "atomize_elim" to convert elimination rules to the object logic
2008-03-20 haftmann 2008-03-20 adjusted authorship
2008-03-10 huffman 2008-03-10 instance fun :: (finite, countable) countable
2008-02-27 haftmann 2008-02-27 added theory for countable types