isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -12 +12 +100 +300 +1000 +3000 +10000 tip

allow registration of custom size functions for BNF-based datatypes
2014-04-23, by blanchet
reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'
2014-04-23, by blanchet
generate 'rec_o_map' and 'size_o_map' in size extension
2014-04-23, by blanchet
made old-style 'size' interpretation hook more robust in case 'size' is already specified (either by the user or by the new datatype package)
2014-04-23, by blanchet
generate size instances for new-style datatypes
2014-04-23, by blanchet
invoke 'fp_sugar' interpretation hook on mutually recursive clique
2014-04-23, by blanchet
declare 'bool' and its proxies as a datatype for SPASS-Pirate
2014-04-23, by blanchet
added 'inj_map' as auxiliary BNF theorem
2014-04-23, by blanchet
tuned whitespace
2014-04-23, by blanchet
remove add_eq_zero_iff, it is replaced by add_nonneg_eq_0_iff; also removes it from the simpset
2014-04-23, by hoelzl
favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;
2014-04-22, by wenzelm
tuned;
2014-04-22, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -12 +12 +100 +300 +1000 +3000 +10000 tip

isabelle