| Mon, 04 Nov 2019 17:06:18 +0000 |
paulson |
Moved or deleted some out of place material, also eliminating obsolete naming conventions
|
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
|
| Fri, 12 Apr 2019 22:09:25 +0200 |
wenzelm |
modernized tags: default scope excludes proof;
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 22:57:16 +0000 |
Angeliki KoutsoukouArgyraki |
minor tagging updates in 13 theories
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:38:00 -0500 |
immler |
subsection is always %important
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:28:07 -0500 |
immler |
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 16:22:21 -0500 |
immler |
revert to 56acd449da41
|
file |
diff |
annotate
|
| Thu, 17 Jan 2019 15:50:28 +0000 |
Angeliki KoutsoukouArgyraki |
more tagging
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 19:48:28 +0100 |
nipkow |
tuned headers; ~ -> \<not>
|
file |
diff |
annotate
|
| Mon, 03 Sep 2018 13:28:52 +0100 |
Angeliki KoutsoukouArgyraki |
tagged 1 theory: Great_Picard
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 14:13:57 +0100 |
paulson |
Generalising and renaming some basic results
|
file |
diff |
annotate
|
| Mon, 21 May 2018 22:52:16 +0100 |
paulson |
small clean-up of Complex_Analysis_Basics
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 12:54:55 +0000 |
paulson |
new material on matrices, etc., and consolidating duplicate results about of_nat
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Tue, 10 Oct 2017 17:15:37 +0100 |
paulson |
Divided Topology_Euclidean_Space in two, creating new theory Connected. Also deleted some duplicate / variant theorems
|
file |
diff |
annotate
|
| Tue, 19 Sep 2017 16:37:19 +0100 |
paulson |
Using the "constant_on" operator
|
file |
diff |
annotate
|
| Thu, 17 Aug 2017 14:52:56 +0200 |
eberlm |
Replaced subseq with strict_mono
|
file |
diff |
annotate
|
| Sun, 14 May 2017 15:35:25 +0200 |
wenzelm |
eliminated suspicious Unicode;
|
file |
diff |
annotate
|
| Thu, 16 Mar 2017 16:02:18 +0000 |
paulson |
Removed [simp] status for Complex_eq. Also tidied some proofs
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 13:51:47 +0000 |
paulson |
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
|
file |
diff |
annotate
|
| Wed, 22 Feb 2017 16:21:26 +0000 |
paulson |
The Great Picard Theorem
|
file |
diff |
annotate
|