| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
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
|
| #
dd59d808 |
|
08-Aug-2016 |
eberlm <eberlm@in.tum.de> |
Tuned primes
|
| #
a2a17ca5 |
|
21-Jul-2016 |
eberlm <eberlm@in.tum.de> |
Overhaul of prime/multiplicity/prime_factors
--HG--
extra : amend_source : bbc753dace9ed5631f671b0800ca8bc5220d1f12
|
| #
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
| #
4b76bc27 |
|
01-Dec-2015 |
paulson <lp15@cam.ac.uk> |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
| #
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
| #
8ddc1a1c |
|
08-Jul-2015 |
haftmann <none@none> |
tuned facts
|
| #
adb7736e |
|
22-Nov-2014 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
b3ac2182 |
|
12-Sep-2013 |
huffman <none@none> |
remove unneeded assumption from prime_dvd_power lemmas;
add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)
--HG--
extra : rebase_source : 3c7a8f4d40859a27cb864cf2a9ade5f7e1cbdead
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
71507759 |
|
15-Apr-2013 |
hoelzl <none@none> |
use automatic type coerctions in Sqrt example
|
| #
b343e07e |
|
15-Feb-2012 |
wenzelm <none@none> |
uniform Isar source formatting for this file;
|
| #
eaa57279 |
|
19-Dec-2011 |
nipkow <none@none> |
added old chestnut
|
| #
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
|
| #
b274c339 |
|
07-Jul-2009 |
nipkow <none@none> |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
| #
f8ffbcd3 |
|
18-Jun-2009 |
huffman <none@none> |
update ex/Sqrt.thy to use new GCD library
|
| #
ba03c6ea |
|
10-Mar-2009 |
wenzelm <none@none> |
tuned proofs;
tuned document;
|
| #
f21befe1 |
|
03-Dec-2008 |
haftmann <none@none> |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML
|