Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
Fri, 04 Sep 2020 17:32:42 +0100 |
paulson |
a bit of tidying
|
file |
diff |
annotate
|
Sun, 30 Aug 2020 19:45:46 +0100 |
paulson |
minor tidying, also s->S and t->T
|
file |
diff |
annotate
|
Wed, 26 Aug 2020 15:59:21 +0100 |
paulson |
tiny tidy-up of proofs
|
file |
diff |
annotate
|
Sat, 23 May 2020 21:24:33 +0100 |
paulson |
a few new lemmas about functions
|
file |
diff |
annotate
|
Tue, 31 Mar 2020 15:51:15 +0200 |
nipkow |
cleaned proofs
|
file |
diff |
annotate
|
Mon, 09 Dec 2019 15:36:51 +0000 |
paulson |
a few new and tidier proofs (mostly about finite sets)
|
file |
diff |
annotate
|
Fri, 06 Dec 2019 17:03:58 +0100 |
nipkow |
cleaning
|
file |
diff |
annotate
|
Thu, 05 Dec 2019 18:26:11 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 05 Dec 2019 11:21:17 +0100 |
nipkow |
made Starlike independent of Abstract_Limits
|
file |
diff |
annotate
|
Wed, 04 Dec 2019 23:11:29 +0100 |
nipkow |
moved starlike where it belongs
|
file |
diff |
annotate
|
Wed, 04 Dec 2019 18:28:24 +0100 |
nipkow |
moved segment lemmas where they belong
|
file |
diff |
annotate
|
Wed, 04 Dec 2019 14:12:59 +0100 |
nipkow |
moved lemmas
|
file |
diff |
annotate
|
Wed, 04 Dec 2019 12:00:07 +0100 |
nipkow |
moved lemma
|
file |
diff |
annotate
|
Fri, 29 Nov 2019 21:29:18 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Fri, 29 Nov 2019 15:06:04 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 28 Nov 2019 23:06:22 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Mon, 04 Nov 2019 19:53:43 -0500 |
immler |
Line_Segment is independent of Convex_Euclidean_Space
|
file |
diff |
annotate
|
Mon, 04 Nov 2019 17:26:20 -0500 |
immler |
betweenness is a property on line segments
|
file |
diff |
annotate
|
Sat, 02 Nov 2019 21:42:45 +0000 |
paulson |
moved line segments to Convex_Euclidean_Space
|
file |
diff |
annotate
|
Sat, 02 Nov 2019 20:51:54 +0000 |
paulson |
just tidied one proof
|
file |
diff |
annotate
|
Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
Tue, 08 Oct 2019 10:26:40 +0000 |
haftmann |
formally augmented corresponding rules for field_simps
|
file |
diff |
annotate
|
Wed, 28 Aug 2019 00:08:14 +0200 |
immler |
removed Brouwer_Fixpoint from imports of Derivative
|
file |
diff |
annotate
|
Fri, 12 Apr 2019 22:24:57 +0200 |
wenzelm |
formal URLs;
|
file |
diff |
annotate
|
Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
Tue, 19 Mar 2019 16:14:51 +0000 |
paulson |
new material about topology, etc.; also fixes for yesterday's
|
file |
diff |
annotate
|
Mon, 18 Mar 2019 15:35:34 +0000 |
paulson |
new material;' strengthened material; moved proofs out of Function_Topology in order to lessen its dependencies
|
file |
diff |
annotate
|
Mon, 28 Jan 2019 10:27:47 +0100 |
nipkow |
more canonical and less specialized syntax
|
file |
diff |
annotate
|
Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
Wed, 16 Jan 2019 19:34:48 -0500 |
immler |
chapters for analysis manual
|
file |
diff |
annotate
|
Wed, 16 Jan 2019 18:14:02 -0500 |
immler |
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
|
file |
diff |
annotate
|
Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
Mon, 07 Jan 2019 13:33:29 +0100 |
immler |
moved setdist to more appropriate places
|
file |
diff |
annotate
|
Sat, 29 Dec 2018 17:46:48 +0100 |
immler |
tuned analysis manual
|
file |
diff |
annotate
|
Sat, 29 Dec 2018 15:43:53 +0100 |
nipkow |
capitalize proper names in lemma names
|
file |
diff |
annotate
|
Fri, 28 Dec 2018 18:53:19 +0100 |
nipkow |
tuned headers etc, added bib-file
|
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, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
Thu, 22 Nov 2018 10:06:31 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
Sun, 11 Nov 2018 16:08:59 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
Thu, 23 Aug 2018 17:09:39 +0000 |
haftmann |
simplified syntax setup for big operators under image, retaining input abbreviations for backward compatibility
|
file |
diff |
annotate
|
Tue, 10 Jul 2018 09:38:35 +0200 |
immler |
make theorem, corollary, and proposition %important for HOL-Analysis manual
|
file |
diff |
annotate
|
Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
Mon, 18 Jun 2018 14:22:26 +0100 |
paulson |
New material in support of quaternions
|
file |
diff |
annotate
|
Thu, 03 May 2018 22:34:49 +0100 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
file |
diff |
annotate
|
Thu, 03 May 2018 16:17:44 +0200 |
immler |
fixed HOL-Analysis
|
file |
diff |
annotate
|
Thu, 03 May 2018 15:07:14 +0200 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
file |
diff |
annotate
|
Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
Wed, 02 May 2018 23:32:47 +0100 |
paulson |
tidying up and using real induction methods
|
file |
diff |
annotate
|
Sun, 29 Apr 2018 21:26:57 +0100 |
paulson |
cleaned up more messy proofs
|
file |
diff |
annotate
|
Mon, 16 Apr 2018 21:23:38 +0100 |
paulson |
some more random results
|
file |
diff |
annotate
|
Mon, 16 Apr 2018 15:00:46 +0100 |
paulson |
more results about measure and negligibility
|
file |
diff |
annotate
|
Sun, 15 Apr 2018 21:41:40 +0100 |
paulson |
quite a few more results about negligibility, etc., and a bit of tidying up
|
file |
diff |
annotate
|
Mon, 09 Apr 2018 16:20:23 +0200 |
nipkow |
removed dots at the end of (sub)titles
|
file |
diff |
annotate
|
Fri, 06 Apr 2018 17:34:50 +0200 |
immler |
a first shot at tagging for HOL-Analysis manual
|
file |
diff |
annotate
|
Thu, 22 Feb 2018 18:01:08 +0100 |
immler |
merged
|
file |
diff |
annotate
|