5 months ago ago CONTRIBUTORS
5 months ago ago Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
5 months ago ago Exponentiation by squaring, fast modular exponentiation
5 months ago ago More material for HOL-Number_Theory: ord, Carmichael's function, primitive roots
6 months ago ago new implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm
8 months ago ago add reconstruction by veriT in method smt
12 months ago ago back to post-release mode -- after fork point;
12 months ago ago Added Real_Asymp package
12 months ago ago tuned;
12 months ago ago merged;
12 months ago ago misc tuning and updates for release;
12 months ago ago merged
12 months ago ago NEWS and CONTRIBUTORS
12 months ago ago Incorporating new/strengthened proofs from Library and AFP entries
12 months ago ago example for Types_To_Sets: transfer from type-based linear algebra to subspaces
13 months ago ago corrections to markup
13 months ago ago updated for release;
14 months ago ago Moved Landau_Symbols from the AFP to HOL-Library
14 months ago ago NEWS and CONTRIBUTORS for 8b50f29a1992
14 months ago ago merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
14 months ago ago added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
15 months ago ago proper datatype for 8-bit characters
15 months ago ago corrected nonsense
16 months ago ago NEWS and CONTRIBUTORS
16 months ago ago Removed stray 'sledgehammer' invocation
18 months ago ago added lemma
19 months ago ago spelling
19 months ago ago a conditional paramitrecity prover
21 months ago ago derived axiom iffI as a lemma (thanks to Alexander Maletzky)
22 months ago ago back to post-release mode -- after fork point;
22 months ago ago tuned;
22 months ago ago Lawrence Paulson's contributions
22 months ago ago listed contribution
22 months ago ago add type of unordered pairs
23 months ago ago tuned;
23 months ago ago HOL-Analysis: Convergent FPS and infinite sums
23 months ago ago misc updates for release;
2017-03-20 ago Corrected affiliation.
2017-03-02 ago Knaster-Tarski fixed point theorem and Galois Connections.
2017-02-22 ago more precise NEWS and CONTRIBUTORS
2017-02-22 ago basic documentation for computations
2016-12-12 ago merged
2016-12-12 ago proper session HOL-Types_To_Sets;
2016-11-01 ago back to post-release mode -- after fork point;
2016-10-31 ago moved contribution to right release
2016-10-25 ago tuned and updated for release;
2016-10-24 ago added Nunchaku integration
2016-10-24 ago Updated NEWS/CONTRIBUTORS w.r.t. Old_Number_Theory
2016-10-07 ago updated for release;
2016-10-03 ago CONTRIBUTORS
2016-09-29 ago CONTRIBUTORS: new proof method "argo"
2016-07-27 ago NEWS: Primes
2016-07-07 ago got rid of class cmp; added height-size proofs by Daniel Stuewe
2016-06-08 ago NEWS and CONTRIBUTORS for SPMF
2016-03-28 ago tuning
2016-03-22 ago document addition of 'corec'
2016-03-18 ago move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-03-03 ago constructive formulation of factorization
2016-02-17 ago prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-02-12 ago merged