2018-07-15 |
Manuel Eberl |
Added Real_Asymp package
|
file |
diff |
annotate
|
2018-06-29 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2018-06-29 |
wenzelm |
merged;
|
file |
diff |
annotate
|
2018-06-29 |
wenzelm |
misc tuning and updates for release;
|
file |
diff |
annotate
|
2018-06-29 |
paulson |
merged
|
file |
diff |
annotate
|
2018-06-28 |
paulson |
Incorporating new/strengthened proofs from Library and AFP entries
|
file |
diff |
annotate
|
2018-06-29 |
Wenda Li |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2018-06-27 |
immler |
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
|
file |
diff |
annotate
|
2018-06-18 |
paulson |
corrections to markup
|
file |
diff |
annotate
|
2018-06-06 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
2018-05-18 |
Manuel Eberl |
Moved Landau_Symbols from the AFP to HOL-Library
|
file |
diff |
annotate
|
2018-05-17 |
Andreas Lochbihler |
NEWS and CONTRIBUTORS for 8b50f29a1992
|
file |
diff |
annotate
|
2018-05-03 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
file |
diff |
annotate
|
2018-05-02 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
2018-04-24 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
2018-04-24 |
haftmann |
corrected nonsense
|
file |
diff |
annotate
|
2018-03-23 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2018-03-12 |
Manuel Eberl |
Removed stray 'sledgehammer' invocation
|
file |
diff |
annotate
|
2018-01-19 |
nipkow |
added lemma
|
file |
diff |
annotate
|
2017-12-25 |
haftmann |
spelling
|
file |
diff |
annotate
|
2017-12-18 |
traytel |
a conditional paramitrecity prover
|
file |
diff |
annotate
|
2017-10-22 |
nipkow |
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
|
file |
diff |
annotate
|
2017-09-08 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
2017-09-08 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2017-09-08 |
paulson |
Lawrence Paulson's contributions
|
file |
diff |
annotate
|
2017-09-08 |
blanchet |
listed contribution
|
file |
diff |
annotate
|
2017-08-30 |
Andreas Lochbihler |
add type of unordered pairs
|
file |
diff |
annotate
|
2017-08-22 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2017-08-21 |
Manuel Eberl |
HOL-Analysis: Convergent FPS and infinite sums
|
file |
diff |
annotate
|
2017-08-21 |
wenzelm |
misc updates for release;
|
file |
diff |
annotate
|
2017-03-20 |
ballarin |
Corrected affiliation.
|
file |
diff |
annotate
|
2017-03-02 |
ballarin |
Knaster-Tarski fixed point theorem and Galois Connections.
|
file |
diff |
annotate
|
2017-02-22 |
haftmann |
more precise NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2017-02-22 |
haftmann |
basic documentation for computations
|
file |
diff |
annotate
|
2016-12-12 |
wenzelm |
merged
|
file |
diff |
annotate
|
2016-12-12 |
wenzelm |
proper session HOL-Types_To_Sets;
|
file |
diff |
annotate
|
2016-11-01 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
2016-10-31 |
blanchet |
moved contribution to right release
|
file |
diff |
annotate
|
2016-10-25 |
wenzelm |
tuned and updated for release;
|
file |
diff |
annotate
|
2016-10-24 |
blanchet |
added Nunchaku integration
|
file |
diff |
annotate
|
2016-10-24 |
eberlm |
Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
|
file |
diff |
annotate
|
2016-10-07 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
2016-10-03 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
2016-09-29 |
boehmes |
CONTRIBUTORS: new proof method "argo"
|
file |
diff |
annotate
|
2016-07-27 |
Manuel Eberl |
NEWS: Primes
|
file |
diff |
annotate
|
2016-07-07 |
nipkow |
got rid of class cmp; added height-size proofs by Daniel Stuewe
|
file |
diff |
annotate
|
2016-06-08 |
Andreas Lochbihler |
NEWS and CONTRIBUTORS for SPMF
|
file |
diff |
annotate
|
2016-03-28 |
blanchet |
tuning
|
file |
diff |
annotate
|
2016-03-22 |
blanchet |
document addition of 'corec'
|
file |
diff |
annotate
|
2016-03-18 |
Andreas Lochbihler |
move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
|
file |
diff |
annotate
|
2016-03-03 |
haftmann |
constructive formulation of factorization
|
file |
diff |
annotate
|
2016-02-17 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
2016-02-12 |
wenzelm |
merged
|
file |
diff |
annotate
|
2016-01-24 |
wenzelm |
more CONTRIBUTORS;
|
file |
diff |
annotate
|
2016-01-20 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
2016-01-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2016-01-19 |
Manuel Eberl |
Added approximation of powr to NEWS/CONTRIBUTORS
|
file |
diff |
annotate
|
2016-01-12 |
paulson |
crediting LCP in CONTRIBUTORS
|
file |
diff |
annotate
|
2016-01-11 |
kleing |
print_record NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2016-01-08 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2016-01-07 |
Manuel Eberl |
Added formal power series updates to NEWS/CONTRIBUTORS
|
file |
diff |
annotate
|
2016-01-06 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
2016-01-06 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
2016-01-05 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
2016-01-05 |
eberlm |
Added summability/Gamma/etc. to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2015-12-31 |
wenzelm |
misc updates for release;
|
file |
diff |
annotate
|
2015-12-19 |
haftmann |
documentation on last state of the art concerning interpretation
|
file |
diff |
annotate
|
2015-12-01 |
Andreas Lochbihler |
add formalisation of Bourbaki-Witt fixpoint theorem
|
file |
diff |
annotate
|
2015-11-02 |
eberlm |
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
|
file |
diff |
annotate
|
2015-08-12 |
traytel |
NEWS, CONTRIBUTORS, documentation for lift_bnf
|
file |
diff |
annotate
|
2015-07-27 |
haftmann |
formal class for factorial (semi)rings
|
file |
diff |
annotate
|
2015-07-08 |
haftmann |
moved normalization and unit_factor into Main HOL corpus
|
file |
diff |
annotate
|
2015-07-02 |
wenzelm |
more CONTRIBUTORS;
|
file |
diff |
annotate
|
2015-06-19 |
haftmann |
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
|
file |
diff |
annotate
|
2015-06-12 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
2015-05-25 |
wenzelm |
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
|
file |
diff |
annotate
|
2015-05-04 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2015-05-04 |
kuncar |
CONTRIBUTORS
|
file |
diff |
annotate
|
2015-04-19 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
2015-04-17 |
wenzelm |
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
|
file |
diff |
annotate
|
2015-04-11 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
2015-04-08 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
2015-03-25 |
blanchet |
more multiset theorems
|
file |
diff |
annotate
|
2014-12-05 |
hoelzl |
add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
|
file |
diff |
annotate
|
2014-10-08 |
Andreas Lochbihler |
move Code_Test to HOL/Library;
|
file |
diff |
annotate
|
2014-09-06 |
haftmann |
theory about lexicographic ordering on functions
|
file |
diff |
annotate
|
2014-08-22 |
haftmann |
generic euclidean algorithm (due to Manuel Eberl)
|
file |
diff |
annotate
|
2014-08-10 |
wenzelm |
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
|
file |
diff |
annotate
|
2014-08-09 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2014-07-30 |
wenzelm |
CONTRIBUTORS;
|
file |
diff |
annotate
|
2014-07-27 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
2014-07-05 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
2014-07-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2014-07-05 |
kleing |
added Tom's hyp_subst update
|
file |
diff |
annotate
|
2014-07-01 |
paulson |
for new release
|
file |
diff |
annotate
|
2014-07-01 |
wenzelm |
misc updates for release;
|
file |
diff |
annotate
|
2014-06-28 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
2014-06-16 |
hoelzl |
lemmas about the moments of the normal distribution
|
file |
diff |
annotate
|
2014-06-13 |
hoelzl |
properties of normal distributed random variables (by Sudeep Kanav)
|
file |
diff |
annotate
|
2014-06-12 |
hoelzl |
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
|
file |
diff |
annotate
|
2014-06-11 |
blanchet |
updated contributors to include students
|
file |
diff |
annotate
|
2014-05-20 |
blanchet |
CONTRIBUTORS
|
file |
diff |
annotate
|
2014-04-05 |
haftmann |
avoid romanism
|
file |
diff |
annotate
|
2014-04-05 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
2014-03-14 |
blanchet |
updated NEWS and CONTRIBUTORS (BNF, SMT2, Sledgehammer)
|
file |
diff |
annotate
|
2014-03-05 |
wenzelm |
proper UTF-8;
|
file |
diff |
annotate
|
2014-03-04 |
nipkow |
added contributor
|
file |
diff |
annotate
|
2014-02-04 |
Lars Hupel |
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
|
file |
diff |
annotate
|
2013-11-11 |
wenzelm |
merged, using src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML and src/HOL/Tools/Sledgehammer/sledgehammer_run.ML from 347c3b0cab44;
|
file |
diff |
annotate
|
2013-11-05 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2013-10-28 |
noschinl |
CONTRIBUTORS
|
file |
diff |
annotate
|
2013-10-03 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
2013-10-03 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2013-10-02 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2013-10-02 |
traytel |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2013-10-02 |
kuncar |
typo
|
file |
diff |
annotate
|
2013-10-02 |
kuncar |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
2013-10-01 |
blanchet |
minor textual changes
|
file |
diff |
annotate
|
2013-09-29 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
2013-09-29 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|