src/HOL/Library/Library.thy
2 months ago ago proper theory for type of dual ordered lattice in distribution
3 months ago ago Exponentiation by squaring, fast modular exponentiation
3 months ago ago the theory of Equipollence, and moving Fpow from Cardinals into Main
6 months ago ago dedicated theory for sorting algorithms
6 months ago ago executable comparators apt for sorting
8 months ago ago Set idioms theory "finite intersection_of open", etc.
12 months ago ago Moved Landau_Symbols from the AFP to HOL-Library
12 months ago ago move FuncSet back to HOL-Library (amending 493b818e8e10)
12 months ago ago new tool Code_Lazy
12 months ago ago merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
12 months ago ago added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
12 months ago ago clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
17 months ago ago a conditional paramitrecity prover
19 months ago ago removed mere toy example from library
20 months ago ago add type of unordered pairs
21 months ago ago reorganization of tree lemmas; new lemmas
21 months ago ago HOL-Library: going_to filter
21 months ago ago syntax for pattern aliases
22 months ago ago state monad
22 months ago ago State_Monad ~> Open_State_Syntax
23 months ago ago specific output setup is not supposed to intrude regular import theory
2017-04-06 ago session containing computational algebra
2017-02-26 ago re-established AFP entry for FinFuns as library
2016-12-17 ago clarified library contents
2016-09-30 ago Library: fix name Product_plus to Product_Plus
2016-09-30 ago HOL-Analysis: move Product_Vector and Inner_Product from Library
2016-09-30 ago HOL-Analysis: move Continuum_Not_Denumerable from Library
2016-09-30 ago HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
2016-09-29 ago Set_Permutations replaced by more general Multiset_Permutations
2016-09-15 ago new type for finite maps; use it in HOL-Probability
2016-09-01 ago clarified session;
2016-07-12 ago more standard name;
2016-07-04 ago combinator to build partial equivalence relations from a predicate and an equivalenc relation
2016-07-04 ago basic facts about almost everywhere fix bijections
2016-06-16 ago Various additions to polynomials, FPSs, Gamma function
2016-05-24 ago Added set permutations/random permutations
2016-05-04 ago move Stirling numbers from AFP/Discrete_Summation
2016-03-22 ago moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-18 ago move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-02-09 ago add extended nonnegative real numbers
2016-02-18 ago add countable complete lattices
2016-02-17 ago separated potentially conflicting type class instance into separate theory
2015-12-01 ago add formalisation of Bourbaki-Witt fixpoint theorem
2015-09-15 ago Omega_Words_Fun: Infinite words as functions from nat.
2015-07-16 ago move disjoint sets to their own theory
2015-04-30 ago tidying some messy proofs
2015-04-21 ago New material, mostly about limits. Consolidation.
2015-04-06 ago new theory Library/Tree_Multiset.thy
2015-03-25 ago more multiset theorems
2014-10-29 ago more standard theory name;
2014-10-08 ago add Linear Temporal Logic on Streams
2014-10-08 ago move Code_Test to HOL/Library;
2014-10-07 ago move Stream theory from Datatype_Examples to Library
2014-09-07 ago explicit theory with additional, less commonly used list operations
2014-09-06 ago theory about sum and product on function bodies
2014-09-06 ago theory about lexicographic ordering on functions
2014-09-01 ago took out legacy material from 'HOL/Library/Library.thy'
2014-08-28 ago renaming theory 'Old_SMT'
2014-08-28 ago moved old 'smt' method out of 'Main'
2014-08-19 ago rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup