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, 06 Apr 2017 21:37:13 +0200 haftmann session containing computational algebra file | diff | annotate
Sun, 26 Feb 2017 13:22:14 +0100 haftmann re-established AFP entry for FinFuns as library file | diff | annotate
Sat, 17 Dec 2016 15:22:13 +0100 haftmann clarified library contents file | diff | annotate
Fri, 30 Sep 2016 15:35:43 +0200 hoelzl Library: fix name Product_plus to Product_Plus file | diff | annotate
Fri, 30 Sep 2016 15:35:37 +0200 hoelzl HOL-Analysis: move Product_Vector and Inner_Product from Library file | diff | annotate
Fri, 30 Sep 2016 15:35:32 +0200 hoelzl HOL-Analysis: move Continuum_Not_Denumerable from Library file | diff | annotate
Fri, 30 Sep 2016 12:00:17 +0200 hoelzl HOL-Analysis: move Library/Convex to Convex_Euclidean_Space file | diff | annotate
Thu, 29 Sep 2016 16:49:42 +0200 eberlm Set_Permutations replaced by more general Multiset_Permutations file | diff | annotate
Thu, 15 Sep 2016 22:41:05 +0200 Lars Hupel new type for finite maps; use it in HOL-Probability file | diff | annotate
Thu, 01 Sep 2016 20:59:51 +0200 wenzelm clarified session; file | diff | annotate
Tue, 12 Jul 2016 19:12:17 +0200 wenzelm more standard name; file | diff | annotate
Mon, 04 Jul 2016 19:46:20 +0200 haftmann combinator to build partial equivalence relations from a predicate and an equivalenc relation file | diff | annotate
Mon, 04 Jul 2016 19:46:20 +0200 haftmann basic facts about almost everywhere fix bijections file | diff | annotate
Thu, 16 Jun 2016 17:57:09 +0200 eberlm Various additions to polynomials, FPSs, Gamma function file | diff | annotate
Tue, 24 May 2016 15:05:41 +0200 eberlm Added set permutations/random permutations file | diff | annotate
Wed, 04 May 2016 10:19:01 +0200 hoelzl move Stirling numbers from AFP/Discrete_Summation file | diff | annotate
Tue, 22 Mar 2016 12:39:37 +0100 blanchet moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle file | diff | annotate
Fri, 18 Mar 2016 08:01:49 +0100 Andreas Lochbihler move Complete_Partial_Orders2 from AFP/Coinductive to HOL/Library file | diff | annotate
Tue, 09 Feb 2016 09:21:10 +0100 hoelzl add extended nonnegative real numbers file | diff | annotate
Thu, 18 Feb 2016 13:54:44 +0100 hoelzl add countable complete lattices file | diff | annotate
Wed, 17 Feb 2016 21:51:58 +0100 haftmann separated potentially conflicting type class instance into separate theory file | diff | annotate
Tue, 01 Dec 2015 12:35:11 +0100 Andreas Lochbihler add formalisation of Bourbaki-Witt fixpoint theorem file | diff | annotate
Tue, 15 Sep 2015 11:18:25 +0200 lammich Omega_Words_Fun: Infinite words as functions from nat. file | diff | annotate
Thu, 16 Jul 2015 10:48:20 +0200 hoelzl move disjoint sets to their own theory file | diff | annotate
Thu, 30 Apr 2015 15:28:01 +0100 paulson tidying some messy proofs file | diff | annotate
Tue, 21 Apr 2015 17:19:00 +0100 paulson New material, mostly about limits. Consolidation. file | diff | annotate
Mon, 06 Apr 2015 15:23:50 +0200 nipkow new theory Library/Tree_Multiset.thy file | diff | annotate
Wed, 25 Mar 2015 17:51:34 +0100 blanchet more multiset theorems file | diff | annotate
Wed, 29 Oct 2014 10:35:00 +0100 wenzelm more standard theory name; file | diff | annotate
Wed, 08 Oct 2014 10:22:00 +0200 hoelzl add Linear Temporal Logic on Streams file | diff | annotate
Wed, 08 Oct 2014 09:09:12 +0200 Andreas Lochbihler move Code_Test to HOL/Library; file | diff | annotate
Tue, 07 Oct 2014 10:48:29 +0200 hoelzl move Stream theory from Datatype_Examples to Library file | diff | annotate
Sun, 07 Sep 2014 09:49:05 +0200 haftmann explicit theory with additional, less commonly used list operations file | diff | annotate
Sat, 06 Sep 2014 20:12:36 +0200 haftmann theory about sum and product on function bodies file | diff | annotate
Sat, 06 Sep 2014 20:12:34 +0200 haftmann theory about lexicographic ordering on functions file | diff | annotate
Mon, 01 Sep 2014 16:17:46 +0200 blanchet took out legacy material from 'HOL/Library/Library.thy' file | diff | annotate
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renaming theory 'Old_SMT' file | diff | annotate
Thu, 28 Aug 2014 00:40:37 +0200 blanchet moved old 'smt' method out of 'Main' file | diff | annotate
Tue, 19 Aug 2014 15:19:16 +0200 Andreas Lochbihler rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup file | diff | annotate
Thu, 12 Jun 2014 21:23:28 +0200 nipkow new theory of binary trees file | diff | annotate
Thu, 29 May 2014 16:13:47 +0200 nipkow removed Kleene_Algebra because of superior AFP entry; authors agreed file | diff | annotate
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas file | diff | annotate
Tue, 13 May 2014 09:21:22 +0200 traytel bnf_decl -> bnf_axiomatization file | diff | annotate
Sat, 05 Apr 2014 10:01:07 +0200 haftmann proper inclusion into library file | diff | annotate
Mon, 10 Mar 2014 20:04:40 +0100 hoelzl 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 file | diff | annotate
Wed, 29 Jan 2014 12:51:37 +0000 paulson Replacing the theory Library/Binomial by Number_Theory/Binomial file | diff | annotate
Fri, 24 Jan 2014 11:51:45 +0100 blanchet killed 'More_BNFs' by moving its various bits where they (now) belong file | diff | annotate
Mon, 20 Jan 2014 18:24:56 +0100 blanchet dissolved BNF session file | diff | annotate
Thu, 16 Jan 2014 16:33:19 +0100 blanchet moved 'Zorn' into 'Main', since it's a BNF dependency file | diff | annotate
Thu, 16 Jan 2014 16:20:17 +0100 blanchet adapted to move of Wfrec file | diff | annotate
Tue, 26 Nov 2013 12:29:31 +0100 hoelzl Add Zorn to HOL-Library file | diff | annotate
Wed, 20 Nov 2013 23:14:06 +0100 blanchet effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies file | diff | annotate
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
less more (0) -100 -60 tip
isabelle