src/HOL/Library/Countable.thy
21 months ago wenzelm 2018-01-11 uniform use of Standard ML op-infix -- eliminated warnings;
21 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
2017-08-18 wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-04-05 Lars Hupel 2017-04-05 use Item_Net to store inductive info
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-03-22 blanchet 2016-03-22 put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints
2016-01-07 paulson 2016-01-07 revisions to limits and derivatives, plus new lemmas
2015-09-04 wenzelm 2015-09-04 modernized name space management -- more uniform qualification;
2015-09-01 wenzelm 2015-09-01 eliminated \<Colon>;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-04-12 wenzelm 2015-04-12 tuned -- avoid ML warnings;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-11 blanchet 2014-09-11 tuning terminology
2014-09-08 blanchet 2014-09-08 compile
2014-09-03 blanchet 2014-09-03 more robust exception handling
2014-09-03 blanchet 2014-09-03 added compatibility function
2014-09-03 blanchet 2014-09-03 added countable tactic for new-style datatypes
2014-09-03 blanchet 2014-09-03 registered 'typerep' as countable again
2014-09-03 blanchet 2014-09-03 commented out failing tactic (now that 'typerep' is defined using the new package
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-06-30 haftmann 2014-06-30 qualified String.explode and String.implode
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
2012-09-06 huffman 2012-09-06 countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-17 wenzelm 2012-03-17 more antiquotations;
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