| Mon, 16 Nov 2020 21:36:07 +0000 |
paulson |
Jakub Kądziołka's stronger version of generate_pow_card (required some restructuring)
|
file |
diff |
annotate
|
| Fri, 17 Jan 2020 18:58:58 +0100 |
Manuel Eberl |
Removed unnecessary and problematic trivial lemma from HOL-Algebra
|
file |
diff |
annotate
|
| Fri, 12 Apr 2019 12:29:20 +0100 |
paulson |
tidying up messy proofs about group element order
|
file |
diff |
annotate
|
| Thu, 11 Apr 2019 22:37:49 +0100 |
paulson |
simpler and stronger proofs
|
file |
diff |
annotate
|
| Tue, 02 Apr 2019 15:23:12 +0100 |
paulson |
The order of a group now follows the HOL Light definition, which is more general
|
file |
diff |
annotate
|
| Tue, 02 Apr 2019 12:56:05 +0100 |
paulson |
some new group theory results: integer group, trivial group, etc.
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 23:23:03 +0100 |
wenzelm |
more formal contributors (with the help of the history);
|
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, 29 Jan 2019 15:26:43 +0000 |
paulson |
some new results in group theory
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 03 Jul 2018 10:07:24 +0100 |
paulson |
even more from Paulo
|
file |
diff |
annotate
|
| Mon, 02 Jul 2018 18:58:50 +0100 |
paulson |
more lemmas from Paulo
|
file |
diff |
annotate
|
| Sun, 01 Jul 2018 20:28:47 +0100 |
paulson |
new lemmas, de-applying, etc.
|
file |
diff |
annotate
|
| Sat, 30 Jun 2018 15:44:04 +0100 |
paulson |
More on Algebra by Paulo and Martin
|
file |
diff |
annotate
|
| Thu, 14 Jun 2018 14:23:38 +0100 |
paulson |
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
|
file |
diff |
annotate
|
| Sat, 12 May 2018 22:20:46 +0200 |
haftmann |
removed some non-essential rules
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 05 Jan 2018 18:41:42 +0100 |
nipkow |
Renamed (^) to [^] in preparation of the move from "op X" to (X)
|
file |
diff |
annotate
|
| Fri, 29 Dec 2017 19:17:52 +0100 |
wenzelm |
prefer formal citations;
|
file |
diff |
annotate
|
| Tue, 19 Dec 2017 13:58:12 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Thu, 24 Aug 2017 17:24:12 +0200 |
haftmann |
more correct output syntax declaration
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 08:33:37 +0200 |
haftmann |
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
|
file |
diff |
annotate
|