improved spelling of formal INCOMPATIBILITY in historic versions (!) -- to avoid ad-hoc word completion multiply such lapses;

merged

tuned spaces

avoid creating needless skolemization steps for SPASS

get rid of 'individual' type in DFG proofs

slightly nicer names

strengthened 'moura' method

improved unskolemization of SPASS problems

more total parser;

more defensive error handling -- token marker must not crash;

merged

documentation of @{cite} and cite_macro;

completion for bibtex entries;

more accurate item name, depending on kind; tuned;

back to liberal spaces of official syntax (in contrast to 4b190c763097), e.g. relevant for easychair.bib;

tuned signature;

add measure space for (coinductive) streams

add type for probability mass functions, i.e. discrete probability distribution

refactor 'map_sel_thms' and 'set_sel_thms'

rename 'xtor_rel_thms' to 'xtor_rels'

rename 'xtor_set_thmss' to 'xtor_setss'

rename 'xtor_map_thms' to 'xtor_maps'

rename one of the two 'rel_eq_thms' to 'rel_code_thms'

rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'

rename 'dtor_set_induct_thms' to 'dtor_set_inducts'

rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'

rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'

add 'set_inducts' to 'fp_sugar'

add 'common_set_inducts' to 'fp_sugar'

add 'rel_co_inducts' to 'fp_sugar'