| Tue, 21 Sep 2021 00:20:47 +0200 |
wenzelm |
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
| Mon, 28 Jun 2021 20:10:23 +0200 |
Andreas Lochbihler |
move code setup from Cardinality to separate theory
|
file |
diff |
annotate
|
| Wed, 05 May 2021 16:09:02 +0000 |
haftmann |
more appropriate location
|
file |
diff |
annotate
|
| Thu, 25 Mar 2021 08:52:15 +0000 |
haftmann |
dedicated session for combinatorial material
|
file |
diff |
annotate
|
| Sun, 28 Feb 2021 20:13:07 +0000 |
haftmann |
dissolve theory with duplicated name from afp
|
file |
diff |
annotate
|
| Tue, 23 Feb 2021 20:41:48 +0000 |
haftmann |
more specific name
|
file |
diff |
annotate
|
| Sat, 02 Jan 2021 23:03:47 +0100 |
wenzelm |
tuned whitespace (amending a4bffc0de967);
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 10:03:03 +0000 |
haftmann |
moved most material from session HOL-Word to Word_Lib in the AFP
|
file |
diff |
annotate
|
| Wed, 23 Sep 2020 11:14:38 +0000 |
haftmann |
more thorough treatment of division, particularly signed division on int and word
|
file |
diff |
annotate
|
| Thu, 18 Jun 2020 09:07:30 +0000 |
haftmann |
bit operations as distinctive library theory
|
file |
diff |
annotate
|
| Sun, 19 Jan 2020 07:50:35 +0100 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 19:58:02 -0500 |
immler |
moved theory Interval_Approximation from the AFP
|
file |
diff |
annotate
|
| Sun, 27 Oct 2019 21:51:14 -0400 |
immler |
moved theory Interval from the AFP
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
clear separation of types for bits (False / True) and Z2 (0 / 1)
|
file |
diff |
annotate
|
| Wed, 03 Apr 2019 16:38:27 +0100 |
paulson |
new theory Library/Poly_Mapping, of almost-everywhere-zero functions
|
file |
diff |
annotate
|
| Thu, 14 Mar 2019 09:46:09 +0100 |
haftmann |
proper theory for type of dual ordered lattice in distribution
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 15:39:37 +0100 |
Manuel Eberl |
Exponentiation by squaring, fast modular exponentiation
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 14:44:52 +0000 |
paulson |
the theory of Equipollence, and moving Fpow from Cardinals into Main
|
file |
diff |
annotate
|
| Fri, 26 Oct 2018 08:20:45 +0000 |
haftmann |
dedicated theory for sorting algorithms
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 12:42:17 +0000 |
haftmann |
executable comparators apt for sorting
|
file |
diff |
annotate
|
| Mon, 17 Sep 2018 15:31:55 +0100 |
paulson |
Set idioms theory "finite intersection_of open", etc.
|
file |
diff |
annotate
|
| Fri, 18 May 2018 17:51:58 +0200 |
Manuel Eberl |
Moved Landau_Symbols from the AFP to HOL-Library
|
file |
diff |
annotate
|
| Tue, 15 May 2018 11:33:43 +0200 |
immler |
move FuncSet back to HOL-Library (amending 493b818e8e10)
|
file |
diff |
annotate
|
| Sat, 12 May 2018 11:24:11 +0200 |
Andreas Lochbihler |
new tool Code_Lazy
|
file |
diff |
annotate
|
| Thu, 03 May 2018 15:07:14 +0200 |
immler |
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
|
file |
diff |
annotate
|
| Wed, 02 May 2018 13:49:38 +0200 |
immler |
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
|
file |
diff |
annotate
|
| Tue, 01 May 2018 20:40:27 +0200 |
wenzelm |
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
|
file |
diff |
annotate
|
| Mon, 18 Dec 2017 16:58:13 +0100 |
traytel |
a conditional paramitrecity prover
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
removed mere toy example from library
|
file |
diff |
annotate
|
| Wed, 30 Aug 2017 18:01:27 +0200 |
Andreas Lochbihler |
add type of unordered pairs
|
file |
diff |
annotate
|
| Fri, 25 Aug 2017 23:09:56 +0200 |
nipkow |
reorganization of tree lemmas; new lemmas
|
file |
diff |
annotate
|
| Wed, 23 Aug 2017 01:05:39 +0200 |
Manuel Eberl |
HOL-Library: going_to filter
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 14:57:23 +0200 |
Lars Hupel |
syntax for pattern aliases
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 20:47:19 +0200 |
Lars Hupel |
state monad
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 17:22:33 +0200 |
Lars Hupel |
State_Monad ~> Open_State_Syntax
|
file |
diff |
annotate
|
| Mon, 05 Jun 2017 15:59:45 +0200 |
haftmann |
specific output setup is not supposed to intrude regular import theory
|
file |
diff |
annotate
|
| 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
|
| 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
|