| Thu, 14 May 2020 13:44:44 +0200 |
Manuel Eberl |
Tuned some proofs in HOL-Analysis
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Wed, 29 Apr 2020 15:16:17 +0100 |
paulson |
A little more tidying up
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 21:53:45 +0100 |
paulson |
moved subset_image_inj into Hilbert_Choice
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 17:48:28 +0100 |
paulson |
Lindelöf spaces and supporting material
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 23:38:55 +0100 |
immler |
most of Topology_Euclidean_Space (now Elementary_Topology) requires fewer dependencies
|
file |
diff |
annotate
|
| Thu, 07 Jun 2018 19:36:12 +0200 |
nipkow |
utilize 'flip'
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 15:27:46 +0100 |
wenzelm |
prefer formal comments;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:48 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 30 Jan 2017 16:10:52 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 23:42:35 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 02 Oct 2016 14:37:50 +0200 |
wenzelm |
eliminated hard tabs;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2016 14:48:49 +0100 |
paulson |
More advanced theorems about retracts, homotopies., etc
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Thu, 30 Jul 2015 09:49:43 +0200 |
Andreas Lochbihler |
add coinduction rule for infinite
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 17:37:06 +0000 |
paulson |
Not a simprule, as it complicates proofs
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:04:24 +0100 |
Andreas Lochbihler |
add stronger version of lemma
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2013 14:24:21 +0100 |
traytel |
Backed out changeset: a8ad7f6dd217---bypassing Main breaks theories that use \<inf> or \<sup>
|
file |
diff |
annotate
|
| Thu, 28 Nov 2013 13:58:12 +0100 |
blanchet |
reduce dependency (toward move to 'HOL')
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 10:20:25 +0100 |
traytel |
drop theorem duplicates
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|
| Fri, 22 Nov 2013 13:42:00 +0100 |
blanchet |
correctly account for dead variables when naming set functions
|
file |
diff |
annotate
|
| Tue, 27 Aug 2013 23:21:12 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 20 Nov 2012 18:59:35 +0100 |
hoelzl |
add Countable_Set theory
|
file |
diff |
annotate
|
| Sat, 03 Mar 2012 21:01:23 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 17:22:49 -0700 |
huffman |
avoid warnings
|
file |
diff |
annotate
|
| Fri, 12 Aug 2011 07:18:28 -0700 |
huffman |
make HOLCF work with separate set type
|
file |
diff |
annotate
|
| Sun, 28 Nov 2010 15:20:51 +0100 |
nipkow |
gave more standard finite set rules simp and intro attribute
|
file |
diff |
annotate
|
| Sat, 20 Mar 2010 02:23:41 +0100 |
Christian Urban |
added lemma infinite_Un
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 10:16:10 -0800 |
huffman |
remove redundant theorem attributes
|
file |
diff |
annotate
|
| Sat, 16 Jan 2010 17:15:28 +0100 |
haftmann |
dropped some old primrecs and some constdefs
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 13:49:36 -0800 |
huffman |
add lemma INFM_conjI
|
file |
diff |
annotate
|
| Thu, 17 Dec 2009 09:33:30 -0800 |
huffman |
added lemmas about INFM/MOST
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 23:55:04 +0100 |
nipkow |
finiteness lemmas
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 16:20:24 +0000 |
chaieb |
Imports Main in order to avoid the typerep problem
|
file |
diff |
annotate
|
| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 01:19:08 +0200 |
huffman |
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 18:11:21 +0100 |
paulson |
fixed ancestors
|
file |
diff |
annotate
|
| Mon, 10 Dec 2007 11:24:09 +0100 |
haftmann |
switched import from Main to PreList
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 23:04:39 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2007 16:25:57 +0100 |
berghofe |
Renamed INF to INFM to avoid clash with INF operator defined in FixedPoint theory.
|
file |
diff |
annotate
|
| Thu, 01 Feb 2007 13:41:19 +0100 |
paulson |
new theorem int_infinite
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:26 +0200 |
wenzelm |
moved theory Infinite_Set to Library;
|
file |
diff |
annotate
|