updated certificates

tuned message

tabled, v.: postpone consideration of

adapted to renaming of 'Projl' and 'Projr'

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'

adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'

renamed 'nat_{case,rec}' to '{case,rec}_nat'

renamed '{prod,sum,bool,unit}_case' to 'case_...'

adapted theories to '{case,rec}_{list,option}' names

avoid old 'prod.simps' -- better be more specific

repaired hard-coded constant names

killed 'rep_compat' option

made 'ctr_sugar' more friendly to the 'datatype_realizer' * * * reverted changes to 'datatype_realizer.ML'

use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture

use right local theory -- shows up when 'no_discs_sels' is set

compatibility names

use new selector support to define 'the', 'hd', 'tl'

transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'

avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'

tuned code

more 'ctr_sugar' modernization

tuning

ported predicate compiler to 'ctr_sugar' * * * ported predicate compiler to 'ctr_sugar', part 2

updated docs

generate 'fundec_cong' attribute for new-style (co)datatypes * * * compile

got rid of dynamic scoping the easy way

removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)

more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's

se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets

have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)