| 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
|