| #
4d8b7cc9 |
|
13-Mar-2020 |
wenzelm <none@none> |
some uses of "' " as witness for this feature;
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
f92cdfe8 |
|
29-Jul-2018 |
paulson <lp15@cam.ac.uk> |
de-applying and removal of obsolete aliases
|
| #
4fa47235 |
|
02-Dec-2017 |
haftmann <none@none> |
generalized more lemmas
--HG--
extra : rebase_source : 4a9e374a2016496ef031305b318725707a19097b
|
| #
05932626 |
|
23-Nov-2017 |
haftmann <none@none> |
generalized more lemmas
|
| #
dc0eecf4 |
|
23-Nov-2017 |
haftmann <none@none> |
tuned
|
| #
f727cf78 |
|
23-Nov-2017 |
haftmann <none@none> |
tuned and generalized
|
| #
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality
--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
| #
6df0c8c4 |
|
31-Oct-2017 |
haftmann <none@none> |
removed ancient nat-int transfer
--HG--
extra : rebase_source : ce8f250636192c6dff622d66fb514fcc401ce0e7
|
| #
9e54613e |
|
20-Oct-2017 |
haftmann <none@none> |
algebraic foundation for congruences
--HG--
extra : rebase_source : 92f02fe56b0c3a5d4e31c87c498019c1c76b5c47
|
| #
c4bc2aff |
|
09-Oct-2017 |
haftmann <none@none> |
tuned proofs
--HG--
extra : rebase_source : f75a8a3d183658e5e8f4190946b69265b54c84c9
|
| #
fd2471a9 |
|
08-Oct-2017 |
haftmann <none@none> |
euclidean rings need no normalization
--HG--
extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
441ebe66 |
|
08-Aug-2017 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
37a4900c |
|
06-Apr-2017 |
haftmann <none@none> |
session containing computational algebra
--HG--
rename : src/HOL/Number_Theory/Euclidean_Algorithm.thy => src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
rename : src/HOL/Number_Theory/Factorial_Ring.thy => src/HOL/Computational_Algebra/Factorial_Ring.thy
rename : src/HOL/Library/Formal_Power_Series.thy => src/HOL/Computational_Algebra/Formal_Power_Series.thy
rename : src/HOL/Library/Fundamental_Theorem_Algebra.thy => src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
rename : src/HOL/Library/Normalized_Fraction.thy => src/HOL/Computational_Algebra/Normalized_Fraction.thy
rename : src/HOL/Library/Polynomial.thy => src/HOL/Computational_Algebra/Polynomial.thy
rename : src/HOL/Library/Polynomial_FPS.thy => src/HOL/Computational_Algebra/Polynomial_FPS.thy
rename : src/HOL/Library/Polynomial_Factorial.thy => src/HOL/Computational_Algebra/Polynomial_Factorial.thy
rename : src/HOL/Number_Theory/Primes.thy => src/HOL/Computational_Algebra/Primes.thy
extra : rebase_source : c81da44950fdb70d0f6e552e1f73b980cac0ac75
|
| #
c32926df |
|
17-Dec-2016 |
haftmann <none@none> |
reoriented congruence rules in non-explosive direction
--HG--
extra : rebase_source : 7b0d0d20a7c78db1ac5f12fb0d4ab0d915d0f2a3
|
| #
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
ad00661e |
|
16-Sep-2016 |
wenzelm <none@none> |
more symbols;
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
0a4555c1 |
|
26-Feb-2016 |
Manuel Eberl <eberlm@in.tum.de> |
Tuned Euclidean Rings/GCD rings
|
| #
069896e9 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings and tuned proofs
|
| #
b376ab94 |
|
17-Feb-2016 |
haftmann <none@none> |
cleansed junk-producing interpretations for gcd/lcm on nat altogether
|
| #
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
| #
d42838c4 |
|
28-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
81da5767 |
|
08-Jul-2015 |
haftmann <none@none> |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
| #
2e53e27d |
|
19-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
8c67c983 |
|
23-Mar-2015 |
haftmann <none@none> |
distributivity of partial minus establishes desired properties of dvd in semirings
--HG--
extra : rebase_source : 99dad957de0410b3a1ca21ff1f8723495b31194f
|
| #
08ee2a04 |
|
10-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
| #
255f0ad6 |
|
17-Nov-2014 |
haftmann <none@none> |
generalized lemmas and tuned proofs
|
| #
3d6a4c68 |
|
07-Nov-2014 |
wenzelm <none@none> |
tuned syntax -- separate tokens;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
0551f7de |
|
01-Nov-2014 |
wenzelm <none@none> |
eliminated spurious semicolons;
|
| #
4a9ed335 |
|
07-Oct-2014 |
wenzelm <none@none> |
more bibtex entries;
more antiquotations;
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
| #
7c47fbfc |
|
09-Feb-2014 |
paulson <lp15@cam.ac.uk> |
tidied messy proofs
|
| #
36c3caae |
|
05-Feb-2014 |
paulson <lp15@cam.ac.uk> |
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
|
| #
134232ec |
|
04-Feb-2014 |
paulson <lp15@cam.ac.uk> |
Restoration of Pocklington.thy. Tidying.
|
| #
89444e58 |
|
02-Feb-2014 |
paulson <lp15@cam.ac.uk> |
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
|
| #
8453c275 |
|
29-Jan-2014 |
paulson <lp15@cam.ac.uk> |
minor adjustments
|
| #
98c6a9db |
|
24-Jan-2014 |
paulson <lp15@cam.ac.uk> |
Restored Suc rather than +1, and using Library/Binimial
|
| #
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
| #
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus
--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
| #
0a8fe6fe |
|
27-Mar-2012 |
huffman <none@none> |
remove redundant lemma
|
| #
184f2f26 |
|
10-Sep-2011 |
wenzelm <none@none> |
misc tuning;
|
| #
6b0b29ec |
|
13-Mar-2011 |
wenzelm <none@none> |
tuned headers;
|
| #
ad3ab16f |
|
13-Jan-2011 |
wenzelm <none@none> |
eliminated global prems;
tuned proofs;
|
| #
27a4ab6b |
|
02-Jun-2010 |
haftmann <none@none> |
avoid duplicate import
|
| #
d1f69b8f |
|
26-Apr-2010 |
haftmann <none@none> |
dropped group_simps, ring_simps, field_eq_simps
|
| #
297293d7 |
|
08-Mar-2010 |
haftmann <none@none> |
transfer: avoid camel case
|
| #
f904cc6f |
|
16-Nov-2009 |
webertj <none@none> |
Fixed a typo in a comment.
|
| #
700fe21b |
|
01-Sep-2009 |
haftmann <none@none> |
some reorganization of number theory
--HG--
rename : src/HOL/NewNumberTheory/Binomial.thy => src/HOL/Number_Theory/Binomial.thy
rename : src/HOL/NewNumberTheory/Cong.thy => src/HOL/Number_Theory/Cong.thy
rename : src/HOL/NewNumberTheory/Fib.thy => src/HOL/Number_Theory/Fib.thy
rename : src/HOL/NewNumberTheory/MiscAlgebra.thy => src/HOL/Number_Theory/MiscAlgebra.thy
rename : src/HOL/GCD.thy => src/HOL/Number_Theory/Primes.thy
rename : src/HOL/NewNumberTheory/ROOT.ML => src/HOL/Number_Theory/ROOT.ML
rename : src/HOL/NewNumberTheory/Residues.thy => src/HOL/Number_Theory/Residues.thy
rename : src/HOL/NewNumberTheory/UniqueFactorization.thy => src/HOL/Number_Theory/UniqueFactorization.thy
rename : src/HOL/NumberTheory/BijectionRel.thy => src/HOL/Old_Number_Theory/BijectionRel.thy
rename : src/HOL/NumberTheory/Chinese.thy => src/HOL/Old_Number_Theory/Chinese.thy
rename : src/HOL/NumberTheory/Euler.thy => src/HOL/Old_Number_Theory/Euler.thy
rename : src/HOL/NumberTheory/EulerFermat.thy => src/HOL/Old_Number_Theory/EulerFermat.thy
rename : src/HOL/NumberTheory/EvenOdd.thy => src/HOL/Old_Number_Theory/EvenOdd.thy
rename : src/HOL/NumberTheory/Factorization.thy => src/HOL/Old_Number_Theory/Factorization.thy
rename : src/HOL/NumberTheory/Fib.thy => src/HOL/Old_Number_Theory/Fib.thy
rename : src/HOL/NumberTheory/Finite2.thy => src/HOL/Old_Number_Theory/Finite2.thy
rename : src/HOL/NumberTheory/Gauss.thy => src/HOL/Old_Number_Theory/Gauss.thy
rename : src/HOL/NumberTheory/Int2.thy => src/HOL/Old_Number_Theory/Int2.thy
rename : src/HOL/NumberTheory/IntFact.thy => src/HOL/Old_Number_Theory/IntFact.thy
rename : src/HOL/NumberTheory/IntPrimes.thy => src/HOL/Old_Number_Theory/IntPrimes.thy
rename : src/HOL/Library/Legacy_GCD.thy => src/HOL/Old_Number_Theory/Legacy_GCD.thy
rename : src/HOL/Library/Pocklington.thy => src/HOL/Old_Number_Theory/Pocklington.thy
rename : src/HOL/Library/Primes.thy => src/HOL/Old_Number_Theory/Primes.thy
rename : src/HOL/NumberTheory/Quadratic_Reciprocity.thy => src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
rename : src/HOL/NumberTheory/ROOT.ML => src/HOL/Old_Number_Theory/ROOT.ML
rename : src/HOL/NumberTheory/Residues.thy => src/HOL/Old_Number_Theory/Residues.thy
rename : src/HOL/NumberTheory/WilsonBij.thy => src/HOL/Old_Number_Theory/WilsonBij.thy
rename : src/HOL/NumberTheory/WilsonRuss.thy => src/HOL/Old_Number_Theory/WilsonRuss.thy
rename : src/HOL/NumberTheory/document/root.tex => src/HOL/Old_Number_Theory/document/root.tex
|