src/HOL/Library/Library.thy
13 months ago Manuel Eberl 2018-05-18 Moved Landau_Symbols from the AFP to HOL-Library
13 months ago immler 2018-05-15 move FuncSet back to HOL-Library (amending 493b818e8e10)
13 months ago Andreas Lochbihler 2018-05-12 new tool Code_Lazy
13 months ago immler 2018-05-03 merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
13 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
13 months ago wenzelm 2018-05-01 clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); tuned headers;
18 months ago traytel 2017-12-18 a conditional paramitrecity prover
20 months ago haftmann 2017-10-08 removed mere toy example from library
21 months ago Andreas Lochbihler 2017-08-30 add type of unordered pairs
22 months ago nipkow 2017-08-25 reorganization of tree lemmas; new lemmas
22 months ago Manuel Eberl 2017-08-23 HOL-Library: going_to filter
22 months ago Lars Hupel 2017-08-18 syntax for pattern aliases
23 months ago Lars Hupel 2017-07-11 state monad
23 months ago Lars Hupel 2017-07-11 State_Monad ~> Open_State_Syntax
2017-06-05 haftmann 2017-06-05 specific output setup is not supposed to intrude regular import theory
2017-04-06 haftmann 2017-04-06 session containing computational algebra
2017-02-26 haftmann 2017-02-26 re-established AFP entry for FinFuns as library
2016-12-17 haftmann 2016-12-17 clarified library contents
2016-09-30 hoelzl 2016-09-30 Library: fix name Product_plus to Product_Plus
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Product_Vector and Inner_Product from Library
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Continuum_Not_Denumerable from Library
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
2016-09-29 eberlm 2016-09-29 Set_Permutations replaced by more general Multiset_Permutations
2016-09-15 Lars Hupel 2016-09-15 new type for finite maps; use it in HOL-Probability
2016-09-01 wenzelm 2016-09-01 clarified session; misc tuning and modernization;
2016-07-12 wenzelm 2016-07-12 more standard name;
2016-07-04 haftmann 2016-07-04 combinator to build partial equivalence relations from a predicate and an equivalenc relation
2016-07-04 haftmann 2016-07-04 basic facts about almost everywhere fix bijections
2016-06-16 eberlm 2016-06-16 Various additions to polynomials, FPSs, Gamma function
2016-05-24 eberlm 2016-05-24 Added set permutations/random permutations
2016-05-04 hoelzl 2016-05-04 move Stirling numbers from AFP/Discrete_Summation
2016-03-22 blanchet 2016-03-22 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
2016-03-18 Andreas Lochbihler 2016-03-18 move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library
2016-02-09 hoelzl 2016-02-09 add extended nonnegative real numbers
2016-02-18 hoelzl 2016-02-18 add countable complete lattices
2016-02-17 haftmann 2016-02-17 separated potentially conflicting type class instance into separate theory
2015-12-01 Andreas Lochbihler 2015-12-01 add formalisation of Bourbaki-Witt fixpoint theorem
2015-09-15 lammich 2015-09-15 Omega_Words_Fun: Infinite words as functions from nat.
2015-07-16 hoelzl 2015-07-16 move disjoint sets to their own theory
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-21 paulson 2015-04-21 New material, mostly about limits. Consolidation.
2015-04-06 nipkow 2015-04-06 new theory Library/Tree_Multiset.thy
2015-03-25 blanchet 2015-03-25 more multiset theorems
2014-10-29 wenzelm 2014-10-29 more standard theory name;
2014-10-08 hoelzl 2014-10-08 add Linear Temporal Logic on Streams
2014-10-08 Andreas Lochbihler 2014-10-08 move Code_Test to HOL/Library; add corresponding entries in NEWS and CONTRIBUTORS
2014-10-07 hoelzl 2014-10-07 move Stream theory from Datatype_Examples to Library
2014-09-07 haftmann 2014-09-07 explicit theory with additional, less commonly used list operations
2014-09-06 haftmann 2014-09-06 theory about sum and product on function bodies
2014-09-06 haftmann 2014-09-06 theory about lexicographic ordering on functions
2014-09-01 blanchet 2014-09-01 took out legacy material from 'HOL/Library/Library.thy'
2014-08-28 blanchet 2014-08-28 renaming theory 'Old_SMT'
2014-08-28 blanchet 2014-08-28 moved old 'smt' method out of 'Main'
2014-08-19 Andreas Lochbihler 2014-08-19 rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-06-12 nipkow 2014-06-12 new theory of binary trees
2014-05-29 nipkow 2014-05-29 removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-20 hoelzl 2014-05-20 add various lemmas
2014-05-13 traytel 2014-05-13 bnf_decl -> bnf_axiomatization
2014-04-05 haftmann 2014-04-05 proper inclusion into library
2014-03-10 hoelzl 2014-03-10 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