Mercurialisabelle / file revisions
summary | shortlog | changelog | graph | tags | branches | file | revisions | annotate | diff | rss
src/HOL/Library/Library.thy
2013-10-31 haftmann 2013-10-31 more convenient place for a theory in solitariness file | diff | annotate
2013-10-31 haftmann 2013-10-31 consolidated clone theory file | diff | annotate
2013-09-27 kuncar 2013-09-27 new theory of finite sets as a subtype file | diff | annotate
2013-05-27 wenzelm 2013-05-27 actually test theory Order_Union; file | diff | annotate
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative file | diff | annotate
2013-03-26 wenzelm 2013-03-26 tuned imports; file | diff | annotate
2013-03-09 haftmann 2013-03-09 discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types file | diff | annotate
2013-03-05 nipkow 2013-03-05 New theory of infinity-extended types; should replace Extended_xyz eventually file | diff | annotate
2013-02-24 haftmann 2013-02-24 turned example into library for comparing growth of functions file | diff | annotate
2013-02-17 haftmann 2013-02-17 fundamentals about discrete logarithm and square root file | diff | annotate
2013-02-15 haftmann 2013-02-15 attempt to re-establish conventions which theories are loaded into the grand unified library theory; four different code generation tests for different code setup constellations; augment code generation setup where necessary file | diff | annotate
2012-11-20 hoelzl 2012-11-20 add Countable_Set theory file | diff | annotate
2012-11-15 immler 2012-11-15 regularity of measures, therefore: characterization of closure with infimum distance; characterize of compact sets as totally bounded; added Diagonal_Subsequence to Library; introduced (enumerable) topological basis; rational boxes as basis of ordered euclidean space; moved some lemmas upwards file | diff | annotate
2012-08-09 wenzelm 2012-08-09 explicit FIXME; file | diff | annotate
2012-07-31 kuncar 2012-07-31 implementation of sets by RBT trees for the code generator file | diff | annotate
2012-07-22 haftmann 2012-07-22 library theories for debugging and parallel computing using code generation towards Isabelle/ML file | diff | annotate
2012-07-17 haftmann 2012-07-17 explicitly import Dlist theory into library file | diff | annotate
2012-07-05 haftmann 2012-07-05 Stub theory for division on functionals. file | diff | annotate
2012-05-29 Andreas Lochbihler 2012-05-29 move FinFuns from AFP to repository file | diff | annotate
2012-03-30 haftmann 2012-03-30 dropped now obsolete Cset theories file | diff | annotate
2011-12-26 haftmann 2011-12-26 incorporated More_Set and More_List into the Main body -- to be consolidated later file | diff | annotate
2011-12-04 huffman 2011-12-04 remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality file | diff | annotate
2011-09-25 haftmann 2011-09-25 Quotient_Set.thy is part of library file | diff | annotate
2011-09-12 bulwahn 2011-09-12 moving connection of association lists to Mappings into a separate theory file | diff | annotate
2011-09-07 haftmann 2011-09-07 theory of saturated naturals contributed by Peter Gammie file | diff | annotate
2011-08-28 haftmann 2011-08-28 avoid loading List_Cset and Dlist_Cet at the same time file | diff | annotate
2011-08-17 wenzelm 2011-08-17 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library); file | diff | annotate
2011-08-16 huffman 2011-08-16 get Library/Permutations.thy compiled and working again file | diff | annotate
2011-08-02 krauss 2011-08-02 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef file | diff | annotate
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy file | diff | annotate
2011-07-26 Andreas Lochbihler 2011-07-26 Add theory for setting up monad syntax for Cset file | diff | annotate
2011-07-25 bulwahn 2011-07-25 removing SML_Quickcheck file | diff | annotate
2011-07-19 hoelzl 2011-07-19 rename Nat_Infinity (inat) to Extended_Nat (enat) file | diff | annotate
2011-06-07 bulwahn 2011-06-07 splitting Cset into Cset and List_Cset file | diff | annotate
2011-06-02 bulwahn 2011-06-02 splitting Dlist theory in Dlist and Dlist_Cset file | diff | annotate
2011-06-01 bulwahn 2011-06-01 splitting RBT theory into RBT and RBT_Mapping file | diff | annotate
2011-01-08 wenzelm 2011-01-08 renamed Sum_Of_Squares to Sum_of_Squares; file | diff | annotate
2010-11-22 haftmann 2010-11-22 merged file | diff | annotate
2010-11-22 haftmann 2010-11-22 replaced misleading Fset/fset name -- these do not stand for finite sets file | diff | annotate
2010-11-22 bulwahn 2010-11-22 adding Enum to HOL-Main image and removing it from HOL-Library file | diff | annotate
2010-11-03 haftmann 2010-11-03 moved theory Quicksort from Library/ to ex/ file | diff | annotate
2010-08-20 haftmann 2010-08-20 split and enriched theory SetsAndFunctions file | diff | annotate
2010-07-14 haftmann 2010-07-14 load cache_io before code generator; moved adhoc-overloading to generic tools file | diff | annotate
2010-07-13 krauss 2010-07-13 uniform do notation for monads file | diff | annotate
2010-07-13 krauss 2010-07-13 generic ad-hoc overloading via check/uncheck file | diff | annotate
2010-07-02 haftmann 2010-07-02 remove codegeneration-related theories from big library theory file | diff | annotate
2010-07-01 hoelzl 2010-07-01 Add theory for indicator function. file | diff | annotate
2010-05-20 haftmann 2010-05-20 added theory More_List file | diff | annotate
2010-05-17 haftmann 2010-05-17 dropped old Library/Word.thy and toy example ex/Adder.thy file | diff | annotate
2010-05-04 hoelzl 2010-05-04 Add Convex to Library build file | diff | annotate
2010-04-15 haftmann 2010-04-15 theory RBT with abstract type of red-black trees backed by implementation RBT_Impl file | diff | annotate
2010-03-13 wenzelm 2010-03-13 removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0; file | diff | annotate
2010-03-06 haftmann 2010-03-06 added Table.thy file | diff | annotate
2010-02-22 haftmann 2010-02-22 added Dlist file | diff | annotate
2010-02-19 Cezary Kaliszyk 2010-02-19 Initial version of HOL quotient package. file | diff | annotate
2010-02-10 wenzelm 2010-02-10 renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL; file | diff | annotate
2010-02-10 haftmann 2010-02-10 revert uninspired Structure_Syntax experiment file | diff | annotate
2010-02-08 haftmann 2010-02-08 merged file | diff | annotate
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures file | diff | annotate
2010-02-08 haftmann 2010-02-08 separate theory for index structures file | diff | annotate
isabelle