src/HOL/Library/Library.thy
21 months ago ago Moved Landau_Symbols from the AFP to HOL-Library
21 months ago ago move FuncSet back to HOL-Library (amending 493b818e8e10)
21 months ago ago new tool Code_Lazy
22 months ago ago merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
22 months ago ago added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
22 months ago ago clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
2017-12-18 ago a conditional paramitrecity prover
2017-10-08 ago removed mere toy example from library
2017-08-30 ago add type of unordered pairs
2017-08-25 ago reorganization of tree lemmas; new lemmas
2017-08-23 ago HOL-Library: going_to filter
2017-08-18 ago syntax for pattern aliases
2017-07-11 ago state monad
2017-07-11 ago State_Monad ~> Open_State_Syntax
2017-06-05 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
2014-06-12 ago new theory of binary trees
2014-05-29 ago removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-20 ago add various lemmas
2014-05-13 ago bnf_decl -> bnf_axiomatization
2014-04-05 ago proper inclusion into library
2014-03-10 ago introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices