| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Wed, 13 Jul 2016 19:02:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 15:45:32 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2016 10:09:20 +0200 |
wenzelm |
bundle lifting_syntax;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Wed, 01 Jun 2016 13:48:34 +0200 |
eberlm |
Tuned code equations for mappings and PMFs
|
file |
diff |
annotate
|
| Tue, 31 May 2016 13:02:44 +0200 |
eberlm |
Added code generation for PMFs
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 20:56:24 +0200 |
wenzelm |
proper qualified naming;
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Jun 2015 11:03:05 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 06 Feb 2015 08:47:48 +0100 |
haftmann |
non-intrusive default code setup for mappings
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 11:27:36 +0200 |
haftmann |
more operations and lemmas
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 14:08:25 +0200 |
haftmann |
restoring notion of primitive vs. derived operations in terms of generated code;
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 14:08:18 +0200 |
haftmann |
removed duplication and tuned
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:29:18 +0100 |
blanchet |
renamed 'prod_rel' to 'rel_prod'
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 14:57:14 +0100 |
blanchet |
renamed 'set_rel' to 'rel_set'
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 21:33:28 +0100 |
blanchet |
folded 'rel_option' into 'option_rel'
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
merged 'Option.map' and 'Option.map_option'
|
file |
diff |
annotate
|
| Mon, 23 Dec 2013 16:29:43 +0100 |
haftmann |
prefer Y_of_X over X_to_Y;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 18:22:55 +0200 |
traytel |
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
remove unnecessary dependencies on Library/Quotient_*
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:21:58 +0100 |
kuncar |
convert mappings to parametric lifting
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:21:06 +0100 |
kuncar |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
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
|
| Wed, 24 Oct 2012 18:43:25 +0200 |
huffman |
transfer package: more flexible handling of equality relations using is_equality predicate
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 22:47:14 +0200 |
kuncar |
new theorems
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 17:54:16 +0200 |
kuncar |
don't include Quotient_Option - workaround to a transfer bug
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 15:52:33 +0200 |
kuncar |
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| 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
|