| Tue, 23 Jul 2024 15:54:43 +0100 |
paulson |
A lot of new material from the Ramsey development, including a couple of new simprules.
|
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
|
| Thu, 24 Aug 2023 21:40:24 +0100 |
paulson |
some refinements in Algebra and Number_Theory
|
file |
diff |
annotate
|
| Wed, 24 Aug 2022 08:22:13 +0000 |
haftmann |
avoid duplicate fact error on global_interpretation of residues
|
file |
diff |
annotate
|
| Fri, 06 Dec 2019 16:22:15 +0100 |
wenzelm |
removed junk;
|
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
|
| Sun, 17 Jun 2018 22:00:43 +0100 |
paulson |
Algebra tidy-up
|
file |
diff |
annotate
|
| Thu, 14 Jun 2018 15:20:10 +0100 |
paulson |
Adjusting Number_Theory for new Algebra
|
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
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 07:11:03 +0000 |
haftmann |
removed ancient nat-int transfer
|
file |
diff |
annotate
|
| Fri, 20 Oct 2017 20:57:55 +0200 |
haftmann |
algebraic foundation for congruences
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:48 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
euclidean rings need no normalization
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Tue, 01 Aug 2017 22:19:37 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 01 Aug 2017 17:33:04 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 22 May 2017 14:08:22 +0200 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Thu, 04 May 2017 16:49:29 +0200 |
eberlm |
More material on totient function
|
file |
diff |
annotate
|
| Wed, 12 Apr 2017 09:27:43 +0200 |
haftmann |
more fundamental euler's totient function on nat rather than int;
|
file |
diff |
annotate
|
| Thu, 06 Apr 2017 08:33:37 +0200 |
haftmann |
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
|
file |
diff |
annotate
|
| Tue, 28 Feb 2017 15:17:57 +0000 |
paulson |
tidied some messy proofs
|
file |
diff |
annotate
|
| Sat, 17 Dec 2016 15:22:14 +0100 |
haftmann |
reoriented congruence rules in non-explosive direction
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 15:20:06 +0200 |
eberlm |
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 08 Aug 2016 17:47:51 +0200 |
eberlm |
is_prime -> prime
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 17:35:54 +0200 |
eberlm |
Removed redundant material related to primes
|
file |
diff |
annotate
|
| Thu, 21 Jul 2016 10:06:04 +0200 |
eberlm |
Overhaul of prime/multiplicity/prime_factors
|
file |
diff |
annotate
|
| Sat, 09 Jul 2016 13:26:16 +0200 |
haftmann |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 14:01:41 +0200 |
haftmann |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 23:51:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 23:40:46 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 21:41:33 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 15:20:40 +0000 |
paulson |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Thu, 06 Feb 2014 23:09:22 +0000 |
paulson |
tidied
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 00:22:48 +0000 |
paulson |
fixed indentation
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 21:48:28 +0000 |
paulson |
new lemmas involving phi from Lehmer AFP entry
|
file |
diff |
annotate
|
| Sun, 02 Feb 2014 19:15:25 +0000 |
paulson |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
file |
diff |
annotate
|
| Sat, 01 Feb 2014 00:32:32 +0000 |
paulson |
version of Fermat's Theorem for type nat
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 10:00:53 +0100 |
haftmann |
more direct simplification rules for 1 div/mod numeral;
|
file |
diff |
annotate
|
| Wed, 29 Jan 2014 15:40:33 +0000 |
paulson |
minor adjustments
|
file |
diff |
annotate
|
| Fri, 29 Nov 2013 08:26:45 +0100 |
traytel |
set_comprehension_pointfree simproc causes to many surprises if enabled by default
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 11:59:48 +0100 |
bulwahn |
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 15:53:48 +0200 |
huffman |
remove redundant lemma
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 23:27:32 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Thu, 13 Jan 2011 23:50:16 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:19 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
| base
|