| Tue, 05 Oct 2010 11:37:42 +0200 |
haftmann |
lemmas fold_commute and fold_commute_apply
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 16:43:23 +0200 |
haftmann |
moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
|
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
|
| Tue, 29 Jun 2010 07:55:18 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:32:06 +0200 |
haftmann |
dropped ancient infix mem; refined code generation operations in List.thy
|
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, 21 May 2010 15:22:36 +0200 |
haftmann |
refined
|
file |
diff |
annotate
|
| Sun, 11 Apr 2010 16:51:05 +0200 |
haftmann |
constructor Mapping replaces AList
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 16:49:37 +0100 |
haftmann |
added ordered_keys
|
file |
diff |
annotate
|
| Wed, 17 Feb 2010 09:48:52 +0100 |
haftmann |
mappings implemented by association lists
|
file |
diff |
annotate
|
| Sun, 31 Jan 2010 14:51:30 +0100 |
haftmann |
more correspondence lemmas between related operations; tuned some proofs
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
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
|
| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:05 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:17 +0100 |
haftmann |
some more primrec
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:44 +0100 |
haftmann |
dropped superfluous code theorems
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 19:12:59 +0200 |
nipkow |
changed filter syntax from : to <-
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:44 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:33:09 +0200 |
haftmann |
slightly tuned
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 11:21:38 +0200 |
haftmann |
tuned: now using function package
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Tue, 28 Mar 2006 12:11:33 +0200 |
schirmer |
renamed map_val to map_ran
|
file |
diff |
annotate
|
| Tue, 28 Mar 2006 12:05:45 +0200 |
schirmer |
added map_val, superseding map_at and substitute
|
file |
diff |
annotate
|
| Thu, 23 Mar 2006 20:03:53 +0100 |
nipkow |
Converted translations to abbbreviations.
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 16:05:34 +0100 |
schirmer |
Added Library/AssocList.thy
|
file |
diff |
annotate
|