| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:56 +0100 |
blanchet |
avoid old 'prod.simps' -- better be more specific
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 16:18:27 +0200 |
Andreas Lochbihler |
fix code equation for RBT_Impl.fold
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 15:05:07 +0200 |
Andreas Lochbihler |
correct definition for skip_black
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 13:03:50 +0200 |
Andreas Lochbihler |
efficient construction of red black trees from sorted associative lists
|
file |
diff |
annotate
|
| Thu, 20 Sep 2012 17:17:20 +0200 |
Andreas Lochbihler |
more efficient code setup
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
a couple of additions to RBT formalization to allow us to implement RBT_Set
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 14:00:26 +0200 |
wenzelm |
updated headers;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2012 11:45:30 +0200 |
Andreas Lochbihler |
move RBT implementation into type class contexts
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 18:17:16 +0200 |
haftmann |
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:19:49 +0100 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
|
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, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
hide popular names R and B
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 15:03:20 +0200 |
haftmann |
prefer fold over foldl
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
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
| base
|