| Wed, 13 May 2020 12:55:33 +0200 |
Manuel Eberl |
new constant power_int in HOL
|
file |
diff |
annotate
|
| Mon, 11 May 2020 11:15:41 +0100 |
paulson |
the Uniq quantifier
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 22:46:55 +0100 |
paulson |
removed more applys
|
file |
diff |
annotate
|
| Sat, 14 Mar 2020 15:58:51 +0000 |
paulson |
tidied up a few little proofs
|
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, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|
| Thu, 29 Aug 2019 12:59:10 +0000 |
haftmann |
more rules for ordered real vector spaces
|
file |
diff |
annotate
|
| Tue, 27 Aug 2019 22:31:21 +0200 |
immler |
explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space
|
file |
diff |
annotate
|
| Mon, 01 Apr 2019 17:02:43 +0100 |
paulson |
A few results in Algebra, and bits for Analysis
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 21:32:36 +0100 |
immler |
moved lemmas up
|
file |
diff |
annotate
|
| Thu, 27 Dec 2018 21:32:34 +0100 |
immler |
prove lemmas in context real_normed_vector
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 09:11:52 +0100 |
haftmann |
removed relics of ASCII syntax for indexed big operators
|
file |
diff |
annotate
|