| Tue, 10 Dec 2019 01:06:39 +0100 |
traytel |
NEWS, CONTRIBUTORS, and documentation
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 12:13:15 -0400 |
immler |
added contributor
|
file |
diff |
annotate
|
| Sat, 11 May 2019 19:08:26 +0200 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| Tue, 30 Apr 2019 13:01:22 +0100 |
paulson |
A bit of de-applying
|
file |
diff |
annotate
|
| Sun, 14 Apr 2019 13:32:26 +0100 |
paulson |
Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
|
file |
diff |
annotate
|
| Tue, 02 Apr 2019 13:15:37 +0200 |
wenzelm |
more material for release;
|
file |
diff |
annotate
|
| Wed, 13 Mar 2019 20:44:39 +0100 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
| Fri, 15 Feb 2019 07:11:11 +0000 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 17:19:04 +0100 |
Manuel Eberl |
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 15:39:37 +0100 |
Manuel Eberl |
Exponentiation by squaring, fast modular exponentiation
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 12:16:03 +0100 |
Manuel Eberl |
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
|
file |
diff |
annotate
|
| Tue, 01 Jan 2019 17:04:53 +0100 |
Andreas Lochbihler |
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
|
file |
diff |
annotate
|
| Tue, 30 Oct 2018 16:24:04 +0100 |
fleury |
add reconstruction by veriT in method smt
|
file |
diff |
annotate
|
| Sun, 22 Jul 2018 21:04:49 +0200 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| Sun, 15 Jul 2018 14:46:57 +0200 |
Manuel Eberl |
Added Real_Asymp package
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 22:50:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 22:14:33 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 20:11:17 +0200 |
wenzelm |
misc tuning and updates for release;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 11:39:40 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 17:14:40 +0100 |
paulson |
Incorporating new/strengthened proofs from Library and AFP entries
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 10:55:05 +0100 |
Wenda Li |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| Wed, 27 Jun 2018 11:16:43 +0200 |
immler |
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
|
file |
diff |
annotate
|
| Mon, 18 Jun 2018 15:56:03 +0100 |
paulson |
corrections to markup
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 11:49:16 +0200 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| Fri, 18 May 2018 17:51:58 +0200 |
Manuel Eberl |
Moved Landau_Symbols from the AFP to HOL-Library
|
file |
diff |
annotate
|
| Thu, 17 May 2018 07:42:33 +0200 |
Andreas Lochbihler |
NEWS and CONTRIBUTORS for 8b50f29a1992
|
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
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 14:17:57 +0000 |
haftmann |
corrected nonsense
|
file |
diff |
annotate
|