| Fri, 21 Oct 2011 11:17:14 +0200 |
bulwahn |
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
|
file |
diff |
annotate
|
| Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
| Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
| Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
mapper for mapping type
|
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, 02 Jul 2010 17:27:44 +0200 |
haftmann |
explicit code_datatype declaration prevents multiple instantiations later on
|
file |
diff |
annotate
|
| Fri, 02 Jul 2010 16:50:53 +0200 |
haftmann |
refrain from using datatype declaration -- opens chance for quickcheck later on
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 22:06:14 +0200 |
haftmann |
hide default, map_entry, map_default
|
file |
diff |
annotate
|
| Mon, 24 May 2010 13:48:57 +0200 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Fri, 21 May 2010 15:22:37 +0200 |
haftmann |
more lemmas about mappings, in particular keys
|
file |
diff |
annotate
|
| Thu, 20 May 2010 17:29:43 +0200 |
haftmann |
operations default, map_entry, map_default; more lemmas
|
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
|
| Sun, 11 Apr 2010 16:51:06 +0200 |
haftmann |
lemma is_empty_empty
|
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 |
more close integration with theory Map
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 17:21:51 +0100 |
hoelzl |
Remove map_compose, replaced by map_map
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 16:55:20 +0200 |
haftmann |
added trees implementing mappings
|
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
|
| Sat, 07 Feb 2009 10:03:09 +0100 |
haftmann |
Isar proof
|
file |
diff |
annotate
|
| Sat, 07 Feb 2009 09:57:03 +0100 |
haftmann |
added bulkload
|
file |
diff |
annotate
|
| Sat, 07 Feb 2009 08:37:42 +0100 |
haftmann |
added bulkload
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 09:05:19 +0100 |
haftmann |
added replace operation
|
file |
diff |
annotate
|
| Mon, 02 Feb 2009 13:56:22 +0100 |
haftmann |
added Mapping.thy to Library
|
file |
diff |
annotate
|