| 2013-08-13 |
traytel |
2013-08-13 |
got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;
|
file | diff | annotate |
| 2013-08-13 |
kuncar |
2013-08-13 |
remove unnecessary dependencies on Library/Quotient_*
|
file | diff | annotate |
| 2013-03-08 |
kuncar |
2013-03-08 |
convert mappings to parametric lifting
|
file | diff | annotate |
| 2013-03-08 |
kuncar |
2013-03-08 |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
file | diff | annotate |
| 2013-02-15 |
haftmann |
2013-02-15 |
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary
|
file | diff | annotate |
| 2012-10-24 |
huffman |
2012-10-24 |
transfer package: more flexible handling of equality relations using is_equality predicate
|
file | diff | annotate |
| 2012-10-22 |
kuncar |
2012-10-22 |
new theorems
|
file | diff | annotate |
| 2012-10-19 |
kuncar |
2012-10-19 |
don't include Quotient_Option - workaround to a transfer bug
|
file | diff | annotate |
| 2012-10-18 |
kuncar |
2012-10-18 |
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
|
file | diff | annotate |
| 2012-10-12 |
wenzelm |
2012-10-12 |
discontinued obsolete typedef (open) syntax;
|
file | diff | annotate |
| 2011-10-21 |
bulwahn |
2011-10-21 |
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
|
file | diff | annotate |
| 2011-01-11 |
haftmann |
2011-01-11 |
"enriched_type" replaces less specific "type_lifting"
|
file | diff | annotate |
| 2010-12-21 |
haftmann |
2010-12-21 |
tuned type_lifting declarations
|
file | diff | annotate |
| 2010-12-06 |
haftmann |
2010-12-06 |
replace `type_mapper` by the more adequate `type_lifting`
|
file | diff | annotate |
| 2010-11-18 |
haftmann |
2010-11-18 |
mapper for mapping type
|
file | diff | annotate |
| 2010-09-13 |
haftmann |
2010-09-13 |
established emerging canonical names *_eqI and *_eq_iff
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
file | diff | annotate |
| 2010-08-27 |
haftmann |
2010-08-27 |
renamed class/constant eq to equal; tuned some instantiations
|
file | diff | annotate |
| 2010-07-02 |
haftmann |
2010-07-02 |
explicit code_datatype declaration prevents multiple instantiations later on
|
file | diff | annotate |
| 2010-07-02 |
haftmann |
2010-07-02 |
refrain from using datatype declaration -- opens chance for quickcheck later on
|
file | diff | annotate |
| 2010-06-02 |
haftmann |
2010-06-02 |
hide default, map_entry, map_default
|
file | diff | annotate |
| 2010-05-24 |
haftmann |
2010-05-24 |
more lemmas
|
file | diff | annotate |
| 2010-05-21 |
haftmann |
2010-05-21 |
more lemmas about mappings, in particular keys
|
file | diff | annotate |
| 2010-05-20 |
haftmann |
2010-05-20 |
operations default, map_entry, map_default; more lemmas
|
file | diff | annotate |
| 2010-04-16 |
wenzelm |
2010-04-16 |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file | diff | annotate |
| 2010-04-11 |
haftmann |
2010-04-11 |
lemma is_empty_empty
|
file | diff | annotate |
| 2010-02-17 |
haftmann |
2010-02-17 |
added ordered_keys
|
file | diff | annotate |
| 2010-02-17 |
haftmann |
2010-02-17 |
more close integration with theory Map
|
file | diff | annotate |
| 2009-11-12 |
hoelzl |
2009-11-12 |
Remove map_compose, replaced by map_map
|
file | diff | annotate |
| 2009-06-04 |
haftmann |
2009-06-04 |
added trees implementing mappings
|
file | diff | annotate |
| 2009-03-23 |
haftmann |
2009-03-23 |
Main is (Complex_Main) base entry point in library theories
|
file | diff | annotate |
| 2009-02-07 |
haftmann |
2009-02-07 |
Isar proof
|
file | diff | annotate |
| 2009-02-07 |
haftmann |
2009-02-07 |
added bulkload
|
file | diff | annotate |
| 2009-02-07 |
haftmann |
2009-02-07 |
added bulkload
|
file | diff | annotate |
| 2009-02-06 |
haftmann |
2009-02-06 |
added replace operation
|
file | diff | annotate |
| 2009-02-02 |
haftmann |
2009-02-02 |
added Mapping.thy to Library
|
file | diff | annotate |