| Sun, 25 Aug 2024 22:54:56 +0200 |
wenzelm |
use nicer notation, following 783406dd051e;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 16:00:59 +0200 |
wenzelm |
use nicer notation, following 783406dd051e;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 15:40:07 +0200 |
wenzelm |
tuned: prefer notation for Pure.type;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 15:02:19 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Thu, 04 Apr 2024 15:29:41 +0200 |
Manuel Eberl |
moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory
|
file |
diff |
annotate
|
| Tue, 30 Jan 2024 16:39:21 +0000 |
paulson |
A few more new theorems taken from AFP entries
|
file |
diff |
annotate
|
| Wed, 01 Feb 2023 20:21:33 +0100 |
wenzelm |
isabelle update -u cite -l "";
|
file |
diff |
annotate
|
| Sun, 26 Dec 2021 11:01:27 +0000 |
paulson |
Tiny additions inspired by Roth development
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 19:52:10 +0100 |
Manuel Eberl |
some algebra material for HOL: characteristic of a ring, algebraic integers
|
file |
diff |
annotate
|
| Tue, 21 Jan 2020 11:02:27 +0100 |
Manuel Eberl |
Removed multiplicativity assumption from normalization_semidom
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 15:16:45 +0000 |
haftmann |
migrated from Nums to Zarith as library for OCaml integer arithmetic
|
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
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
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
|
| Sun, 23 Sep 2018 15:42:19 +0200 |
nipkow |
more standard syntax
|
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
|
| Thu, 23 Aug 2018 17:09:37 +0000 |
haftmann |
dropped redundant syntax translation rules for big operators
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 23:09:21 +0100 |
paulson |
de-applying
|
file |
diff |
annotate
|
| Thu, 24 May 2018 09:26:26 +0000 |
haftmann |
treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Mon, 30 Oct 2017 13:18:41 +0000 |
haftmann |
tuned some proofs and added some lemmas
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:47 +0200 |
haftmann |
tuned imports
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:20 +0200 |
haftmann |
avoid trivial definition
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 11 May 2017 16:47:53 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|