| Thu, 18 Nov 2010 18:53:36 +0100 |
haftmann |
proper qualification needed due to shadowing on theory merge
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:43:23 +0200 |
haftmann |
established emerging canonical names *_eqI and *_eq_iff
|
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
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Fri, 18 Jun 2010 15:26:02 +0200 |
haftmann |
prefer fold over foldl
|
file |
diff |
annotate
|
| Fri, 21 May 2010 15:22:37 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 20 May 2010 17:29:43 +0200 |
haftmann |
implement Mapping.map_entry
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 11:23:04 +0200 |
hoelzl |
merged
|
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
|
| Sat, 06 Mar 2010 15:31:30 +0100 |
haftmann |
some lemma refinements
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 09:58:28 +0100 |
haftmann |
added bulkload; tuned document
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 17:55:14 +0100 |
haftmann |
moved lemma map_sorted_distinct_set_unique
|
file |
diff |
annotate
|
| Fri, 05 Mar 2010 17:51:29 +0100 |
haftmann |
various refinements
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 17:21:45 +0100 |
haftmann |
restructured RBT theory
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 08:28:33 +0100 |
haftmann |
more explicit naming scheme
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 08:49:03 +0200 |
krauss |
tuned
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 22:50:04 +0200 |
krauss |
added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 10:05:11 +0100 |
haftmann |
normalized imports
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:47:20 +0100 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Mon, 03 Mar 2008 14:03:19 +0100 |
krauss |
new theory of red-black trees, an efficient implementation of finite maps.
|
file |
diff |
annotate
|