src/HOL/Library/Infinite_Set.thy
Thu, 05 Nov 2015 10:39:49 +0100 wenzelm isabelle update_cartouches -c -t;
Thu, 30 Jul 2015 09:49:43 +0200 Andreas Lochbihler add coinduction rule for infinite
Wed, 17 Jun 2015 11:03:05 +0200 wenzelm isabelle update_cartouches;
Sun, 12 Apr 2015 11:34:09 +0200 hoelzl move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
Tue, 10 Feb 2015 17:37:06 +0000 paulson Not a simprule, as it complicates proofs
Tue, 10 Feb 2015 12:04:24 +0100 Andreas Lochbihler add stronger version of lemma
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 17:20:45 +0100 wenzelm modernized header;
Fri, 29 Nov 2013 14:24:21 +0100 traytel Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
Thu, 28 Nov 2013 13:58:12 +0100 blanchet reduce dependency (toward move to 'HOL')
Mon, 25 Nov 2013 10:20:25 +0100 traytel drop theorem duplicates
Mon, 25 Nov 2013 10:14:29 +0100 traytel eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
Fri, 22 Nov 2013 13:42:00 +0100 blanchet correctly account for dead variables when naming set functions
Tue, 27 Aug 2013 23:21:12 +0200 wenzelm tuned proofs;
Tue, 20 Nov 2012 18:59:35 +0100 hoelzl add Countable_Set theory
Sat, 03 Mar 2012 21:01:23 +0100 haftmann tuned whitespace
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Mon, 22 Aug 2011 17:22:49 -0700 huffman avoid warnings
Fri, 12 Aug 2011 07:18:28 -0700 huffman make HOLCF work with separate set type
Sun, 28 Nov 2010 15:20:51 +0100 nipkow gave more standard finite set rules simp and intro attribute
Sat, 20 Mar 2010 02:23:41 +0100 Christian Urban added lemma infinite_Un
Sun, 07 Feb 2010 10:16:10 -0800 huffman remove redundant theorem attributes
Sat, 16 Jan 2010 17:15:28 +0100 haftmann dropped some old primrecs and some constdefs
Thu, 17 Dec 2009 13:49:36 -0800 huffman add lemma INFM_conjI
Thu, 17 Dec 2009 09:33:30 -0800 huffman added lemmas about INFM/MOST
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Fri, 13 Feb 2009 23:55:04 +0100 nipkow finiteness lemmas
Mon, 09 Feb 2009 16:20:24 +0000 chaieb Imports Main in order to avoid the typerep problem
Mon, 07 Jul 2008 08:47:17 +0200 haftmann absolute imports of HOL/*.thy theories
Tue, 01 Jul 2008 01:19:08 +0200 huffman rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Mon, 17 Dec 2007 18:11:21 +0100 paulson fixed ancestors
Mon, 10 Dec 2007 11:24:09 +0100 haftmann switched import from Main to PreList
Thu, 14 Jun 2007 23:04:39 +0200 wenzelm tuned proofs;
Sat, 10 Mar 2007 16:25:57 +0100 berghofe Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.
Thu, 01 Feb 2007 13:41:19 +0100 paulson new theorem int_infinite
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 08 Nov 2006 23:11:13 +0100 wenzelm moved theories Parity, GCD, Binomial to Library;
Tue, 07 Nov 2006 11:47:57 +0100 wenzelm renamed 'const_syntax' to 'notation';
Sun, 01 Oct 2006 18:29:26 +0200 wenzelm moved theory Infinite_Set to Library;
less more (0) tip