| 20 months ago |
Mathias Fleury |
early inclusion of cvc5 proof reconstruction; slightly reorganize smt/z3_reals;
|
file |
diff |
annotate
|
| 21 months ago |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2022-10-14 |
nipkow |
new contributor
|
file |
diff |
annotate
|
| 2022-10-02 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 2022-09-09 |
wenzelm |
tuning and updates for release;
|
file |
diff |
annotate
|
| 2022-09-02 |
wenzelm |
more CONTRIBUTORS + NEWS;
|
file |
diff |
annotate
|
| 2022-07-04 |
haftmann |
officical abstract characters for code generation
|
file |
diff |
annotate
|
| 2022-06-27 |
traytel |
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2022-04-03 |
haftmann |
adjusted printing of type annotations to accomodate Scala 3
|
file |
diff |
annotate
|
| 2022-04-01 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| 2022-03-29 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2022-02-22 |
wenzelm |
various improvements to Isabelle/VSCode (by Denis Paluca and Fabian Huch);
|
file |
diff |
annotate
|
| 2021-11-12 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| 2021-11-03 |
wenzelm |
improved HTML presentation by Fabian Huch;
|
file |
diff |
annotate
|
| 2021-10-26 |
wenzelm |
more CONTRIBUTORS and NEWS;
|
file |
diff |
annotate
|
| 2021-10-07 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2021-10-06 |
eberlm |
new notion of infinite sums in HOL-Analysis, ordering on complex numbers
|
file |
diff |
annotate
|
| 2021-10-07 |
desharna |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2021-10-04 |
wenzelm |
more NEWS and CONTRIBUTORS;
|
file |
diff |
annotate
|
| 2021-10-02 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2021-07-17 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
| 2021-07-08 |
desharna |
added documentation for changes to Sledgehammer option "lam_trans"
|
file |
diff |
annotate
|
| 2021-03-31 |
nipkow |
new automatic order prover: stateless, complete, verified
|
file |
diff |
annotate
|
| 2021-03-25 |
haftmann |
dedicated session for combinatorial material
|
file |
diff |
annotate
|
| 2021-03-19 |
wenzelm |
more CONTRIBUTORS;
|
file |
diff |
annotate
|
| 2021-03-17 |
wenzelm |
more Isabelle symbol definitions for Z Notation, based on https://github.com/isabelle-utp/Z_Toolkit 998c9f7880d3 by Simon Foster;
|
file |
diff |
annotate
|
| 2021-02-19 |
Manuel Eberl |
HOL-Analysis/Probability: Hoeffding's inequality, negative binomial distribution, etc.
|
file |
diff |
annotate
|
| 2021-01-31 |
Andreas Lochbihler |
contributors
|
file |
diff |
annotate
|
| 2021-01-24 |
wenzelm |
merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS;
|
file |
diff |
annotate
|
| 2021-01-17 |
wenzelm |
revert 1105c42722dc on isabelle-release branch;
|
file |
diff |
annotate
|
| 2021-01-14 |
paulson |
new magerial from Jakub Kądziołka
|
file |
diff |
annotate
|
| 2021-01-10 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| 2021-01-10 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2021-01-08 |
Manuel Eberl |
HOL-Data_Structures: added Selection and time functions for list functions
|
file |
diff |
annotate
|
| 2021-01-06 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2020-12-29 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
| 2020-12-27 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2020-12-21 |
wenzelm |
misc tuning for release;
|
file |
diff |
annotate
|
| 2020-12-21 |
wenzelm |
rebuild component with proper ZIPPERPOSITION_HOME for sledgehammer;
|
file |
diff |
annotate
|
| 2020-12-04 |
nipkow |
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
|
file |
diff |
annotate
|
| 2020-11-26 |
nipkow |
removed assumptions in lemma (Stepan Holub)
|
file |
diff |
annotate
|
| 2020-11-16 |
paulson |
Jakub Kądziołka's stronger version of generate_pow_card (required some restructuring)
|
file |
diff |
annotate
|
| 2020-11-15 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
| 2020-10-29 |
desharna |
Added smt (verit) to Sledgehammer's proof preplay.
|
file |
diff |
annotate
|
| 2020-10-19 |
desharna |
Added contributors
|
file |
diff |
annotate
|
| 2020-10-15 |
wenzelm |
proper Isabelle component settings: prefer standard terminology "ISABELLE_VERIT", avoid conflict of "VERIT_VERSION" with processing of implicit options by veriT;
|
file |
diff |
annotate
|
| 2020-09-25 |
haftmann |
factored out typedef material
|
file |
diff |
annotate
|
| 2020-09-17 |
haftmann |
NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2020-08-13 |
wenzelm |
more documentation;
|
file |
diff |
annotate
|
| 2020-08-06 |
wenzelm |
discontinued old batch-build functionality;
|
file |
diff |
annotate
|
| 2020-07-09 |
desharna |
Update Metis to 2.4
|
file |
diff |
annotate
|
| 2020-07-02 |
haftmann |
extraction of equations x = t from premises beneath meta-all
|
file |
diff |
annotate
|
| 2020-06-26 |
wenzelm |
more CONTRIBUTORS;
|
file |
diff |
annotate
|
| 2020-06-18 |
haftmann |
build bit operations on word on library theory on bit operations
|
file |
diff |
annotate
|
| 2020-06-18 |
haftmann |
bit operations as distinctive library theory
|
file |
diff |
annotate
|
| 2020-03-15 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| 2020-02-26 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2020-02-25 |
wenzelm |
update to WebviewPanel API, following initial version by Peter Zeller;
|
file |
diff |
annotate
|
| 2020-02-11 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2020-02-11 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2020-02-11 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2020-02-11 |
paulson |
some lemmas about the lex ordering on lists, etc.
|
file |
diff |
annotate
|
| 2020-02-10 |
wenzelm |
updated for release;
|
file |
diff |
annotate
|
| 2019-12-10 |
traytel |
NEWS, CONTRIBUTORS, and documentation
|
file |
diff |
annotate
|
| 2019-10-27 |
immler |
added contributor
|
file |
diff |
annotate
|
| 2019-05-11 |
wenzelm |
back to post-release mode;
|
file |
diff |
annotate
|
| 2019-04-30 |
paulson |
A bit of de-applying
|
file |
diff |
annotate
|
| 2019-04-14 |
paulson |
Group theory developments towards proving algebraic closure (by de Vilhena and Baillon)
|
file |
diff |
annotate
|
| 2019-04-02 |
wenzelm |
more material for release;
|
file |
diff |
annotate
|
| 2019-03-13 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
| 2019-02-15 |
haftmann |
CONTRIBUTORS
|
file |
diff |
annotate
|
| 2019-02-04 |
Manuel Eberl |
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
|
file |
diff |
annotate
|
| 2019-02-04 |
Manuel Eberl |
Exponentiation by squaring, fast modular exponentiation
|
file |
diff |
annotate
|
| 2019-02-04 |
Manuel Eberl |
More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
|
file |
diff |
annotate
|
| 2019-01-01 |
Andreas Lochbihler |
new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
|
file |
diff |
annotate
|
| 2018-10-30 |
fleury |
add reconstruction by veriT in method smt
|
file |
diff |
annotate
|
| 2018-07-22 |
wenzelm |
back to post-release mode -- after fork point;
|
file |
diff |
annotate
|
| 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
|