Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Library.thy
Thu, 31 Oct 2013 11:44:20 +0100 haftmann more convenient place for a theory in solitariness file | diff | annotate
Thu, 31 Oct 2013 11:44:20 +0100 haftmann consolidated clone theory file | diff | annotate
Fri, 27 Sep 2013 14:43:26 +0200 kuncar new theory of finite sets as a subtype file | diff | annotate
Mon, 27 May 2013 22:32:28 +0200 wenzelm actually test theory Order_Union; file | diff | annotate
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl 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
Tue, 26 Mar 2013 20:02:02 +0100 wenzelm tuned imports; file | diff | annotate
Sat, 09 Mar 2013 11:56:01 +0100 haftmann discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types file | diff | annotate
Tue, 05 Mar 2013 15:26:57 +0100 nipkow New theory of infinity-extended types; should replace Extended_xyz eventually file | diff | annotate
Sun, 24 Feb 2013 20:29:13 +0100 haftmann turned example into library for comparing growth of functions file | diff | annotate
Sun, 17 Feb 2013 22:56:54 +0100 haftmann fundamentals about discrete logarithm and square root file | diff | annotate
Fri, 15 Feb 2013 11:47:34 +0100 haftmann attempt to re-establish conventions which theories are loaded into the grand unified library theory; file | diff | annotate
Tue, 20 Nov 2012 18:59:35 +0100 hoelzl add Countable_Set theory file | diff | annotate
Thu, 15 Nov 2012 10:49:58 +0100 immler regularity of measures, therefore: file | diff | annotate
Thu, 09 Aug 2012 14:09:36 +0200 wenzelm explicit FIXME; file | diff | annotate
Tue, 31 Jul 2012 13:55:39 +0200 kuncar implementation of sets by RBT trees for the code generator file | diff | annotate
Sun, 22 Jul 2012 09:56:34 +0200 haftmann library theories for debugging and parallel computing using code generation towards Isabelle/ML file | diff | annotate
Tue, 17 Jul 2012 23:11:27 +0200 haftmann explicitly import Dlist theory into library file | diff | annotate
Thu, 05 Jul 2012 13:24:09 +0200 haftmann Stub theory for division on functionals. file | diff | annotate
Tue, 29 May 2012 15:31:58 +0200 Andreas Lochbihler move FinFuns from AFP to repository file | diff | annotate
Fri, 30 Mar 2012 18:56:02 +0200 haftmann dropped now obsolete Cset theories file | diff | annotate
Mon, 26 Dec 2011 22:17:10 +0100 haftmann incorporated More_Set and More_List into the Main body -- to be consolidated later file | diff | annotate
Sun, 04 Dec 2011 13:10:19 +0100 huffman remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality file | diff | annotate
Sun, 25 Sep 2011 09:37:33 +0200 haftmann Quotient_Set.thy is part of library file | diff | annotate
Mon, 12 Sep 2011 10:57:58 +0200 bulwahn moving connection of association lists to Mappings into a separate theory file | diff | annotate
Wed, 07 Sep 2011 23:38:52 +0200 haftmann theory of saturated naturals contributed by Peter Gammie file | diff | annotate
Sun, 28 Aug 2011 08:13:30 +0200 haftmann avoid loading List_Cset and Dlist_Cet at the same time file | diff | annotate
Wed, 17 Aug 2011 13:14:20 +0200 wenzelm moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library); file | diff | annotate
Tue, 16 Aug 2011 07:06:54 -0700 huffman get Library/Permutations.thy compiled and working again file | diff | annotate
Tue, 02 Aug 2011 11:52:57 +0200 krauss moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef file | diff | annotate
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy file | diff | annotate
Tue, 26 Jul 2011 10:49:34 +0200 Andreas Lochbihler Add theory for setting up monad syntax for Cset file | diff | annotate
Mon, 25 Jul 2011 10:43:14 +0200 bulwahn removing SML_Quickcheck file | diff | annotate
Tue, 19 Jul 2011 14:35:44 +0200 hoelzl rename Nat_Infinity (inat) to Extended_Nat (enat) file | diff | annotate
Tue, 07 Jun 2011 11:12:05 +0200 bulwahn splitting Cset into Cset and List_Cset file | diff | annotate
Thu, 02 Jun 2011 08:55:08 +0200 bulwahn splitting Dlist theory in Dlist and Dlist_Cset file | diff | annotate
Wed, 01 Jun 2011 09:10:13 +0200 bulwahn splitting RBT theory into RBT and RBT_Mapping file | diff | annotate
Sat, 08 Jan 2011 17:39:51 +0100 wenzelm renamed Sum_Of_Squares to Sum_of_Squares; file | diff | annotate
Mon, 22 Nov 2010 17:49:12 +0100 haftmann merged file | diff | annotate
Mon, 22 Nov 2010 17:46:51 +0100 haftmann replaced misleading Fset/fset name -- these do not stand for finite sets file | diff | annotate
Mon, 22 Nov 2010 11:34:56 +0100 bulwahn adding Enum to HOL-Main image and removing it from HOL-Library file | diff | annotate
Wed, 03 Nov 2010 12:20:33 +0100 haftmann moved theory Quicksort from Library/ to ex/ file | diff | annotate
Fri, 20 Aug 2010 17:48:30 +0200 haftmann split and enriched theory SetsAndFunctions file | diff | annotate
Wed, 14 Jul 2010 14:16:12 +0200 haftmann load cache_io before code generator; moved adhoc-overloading to generic tools file | diff | annotate
Tue, 13 Jul 2010 00:15:37 +0200 krauss uniform do notation for monads file | diff | annotate
Tue, 13 Jul 2010 00:15:37 +0200 krauss generic ad-hoc overloading via check/uncheck file | diff | annotate
Fri, 02 Jul 2010 14:23:17 +0200 haftmann remove codegeneration-related theories from big library theory file | diff | annotate
Thu, 01 Jul 2010 11:48:42 +0200 hoelzl Add theory for indicator function. file | diff | annotate
Thu, 20 May 2010 16:35:54 +0200 haftmann added theory More_List file | diff | annotate
Mon, 17 May 2010 10:58:31 +0200 haftmann dropped old Library/Word.thy and toy example ex/Adder.thy file | diff | annotate
Tue, 04 May 2010 18:05:22 +0200 hoelzl Add Convex to Library build file | diff | annotate
Thu, 15 Apr 2010 12:27:14 +0200 haftmann theory RBT with abstract type of red-black trees backed by implementation RBT_Impl file | diff | annotate
Sat, 13 Mar 2010 17:19:12 +0100 wenzelm removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0; file | diff | annotate
Sat, 06 Mar 2010 15:31:30 +0100 haftmann added Table.thy file | diff | annotate
Mon, 22 Feb 2010 15:53:18 +0100 haftmann added Dlist file | diff | annotate
Fri, 19 Feb 2010 13:54:19 +0100 Cezary Kaliszyk Initial version of HOL quotient package. file | diff | annotate
Wed, 10 Feb 2010 19:37:34 +0100 wenzelm renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL; file | diff | annotate
Wed, 10 Feb 2010 14:12:02 +0100 haftmann revert uninspired Structure_Syntax experiment file | diff | annotate
Mon, 08 Feb 2010 14:08:32 +0100 haftmann merged file | diff | annotate
Mon, 08 Feb 2010 14:06:41 +0100 haftmann separate library theory for type classes combining lattices with various algebraic structures file | diff | annotate
Mon, 08 Feb 2010 10:36:02 +0100 haftmann separate theory for index structures file | diff | annotate
less more (0) -100 -60 tip
isabelle