src/HOL/Library/Infinite_Set.thy
20 months ago wenzelm 2018-01-12 prefer formal comments;
23 months ago haftmann 2017-10-09 tuned proofs
2017-01-30 wenzelm 2017-01-30 misc tuning and modernization;
2016-12-28 wenzelm 2016-12-28 tuned;
2016-10-02 wenzelm 2016-10-02 eliminated hard tabs;
2016-07-14 paulson 2016-07-14 More advanced theorems about retracts, homotopies., etc
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-09 paulson 2015-12-09 sorted out eventually_mono
2015-12-01 paulson 2015-12-01 Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
2015-11-05 wenzelm 2015-11-05 isabelle update_cartouches -c -t;
2015-07-30 Andreas Lochbihler 2015-07-30 add coinduction rule for infinite
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-04-12 hoelzl 2015-04-12 move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
2015-02-10 paulson 2015-02-10 Not a simprule, as it complicates proofs
2015-02-10 Andreas Lochbihler 2015-02-10 add stronger version of lemma
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-11-02 wenzelm 2014-11-02 modernized header;
2013-11-29 traytel 2013-11-29 Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
2013-11-28 blanchet 2013-11-28 reduce dependency (toward move to 'HOL')
2013-11-25 traytel 2013-11-25 drop theorem duplicates
2013-11-25 traytel 2013-11-25 eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
2013-11-22 blanchet 2013-11-22 correctly account for dead variables when naming set functions
2013-08-27 wenzelm 2013-08-27 tuned proofs;
2012-11-20 hoelzl 2012-11-20 add Countable_Set theory
2012-03-03 haftmann 2012-03-03 tuned whitespace
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-08-22 huffman 2011-08-22 avoid warnings
2011-08-12 huffman 2011-08-12 make HOLCF work with separate set type
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-03-20 Christian Urban 2010-03-20 added lemma infinite_Un
2010-02-07 huffman 2010-02-07 remove redundant theorem attributes
2010-01-16 haftmann 2010-01-16 dropped some old primrecs and some constdefs
2009-12-17 huffman 2009-12-17 add lemma INFM_conjI
2009-12-17 huffman 2009-12-17 added lemmas about INFM/MOST
2009-03-23 haftmann 2009-03-23 Main is (Complex_Main) base entry point in library theories
2009-02-13 nipkow 2009-02-13 finiteness lemmas
2009-02-09 chaieb 2009-02-09 Imports Main in order to avoid the typerep problem
2008-07-07 haftmann 2008-07-07 absolute imports of HOL/*.thy theories
2008-07-01 huffman 2008-07-01 rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
2008-06-26 haftmann 2008-06-26 established Plain theory and image
2007-12-17 paulson 2007-12-17 fixed ancestors
2007-12-10 haftmann 2007-12-10 switched import from Main to PreList
2007-06-14 wenzelm 2007-06-14 tuned proofs;
2007-03-10 berghofe 2007-03-10 Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.
2007-02-01 paulson 2007-02-01 new theorem int_infinite
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-08 wenzelm 2006-11-08 moved theories Parity, GCD, Binomial to Library;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-10-01 wenzelm 2006-10-01 moved theory Infinite_Set to Library;