tuned IArray code generator w.r.t. map rel set

ported Nitpick_Examples to new datatypes

set 'fundef_cong' attribute also for (co)datatypes with no live type variables

ported IArray to new datatypes

prevent infinite loop when type variables are of a non-'type' sort

tuned code

ported MicroJava to new datatypes

rename_tac'd scrips

ported Unix to new datatypes

ported Isar_Examples to new datatypes

ported Decision_Procs to new datatypes

ported Induct to new datatypes

half-ported Imperative HOL to new datatypes

generalized 'datatype' LaTeX antiquotation and added 'codatatype'

tuned messages

rename_tac'd scripts

reverted 83a8570b44bc, which was a misunderstanding

rename_tac'd script

ported Bali to new datatypes

rename_tac'd scripts

use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries

merged

enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc

Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new

more docs

more documentation

made 'lifting' plugin more robust

tuned command descriptions

generate better internal names, with name of the target type in it

removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)

added flag to 'typedef' to allow concealed definitions

ported old Nominal to use new datatypes

made tactic even more robust w.r.t. dead variables

made N2M work with sort constraints (cf. TODO)

compile

honour sorts in N2M

proper sort constraints in map and rel theorems

made new countable tactic work with sorts other than 'type'

adapted examples to latest changes

made code work also in the presence of deads

export right sorts

test sorts

use right sort constraints

never include hidden names -- these cannot be referenced afterward

use compatibility layer

made SML/NJ happire

export useful functions for users of (co)recursors

improved caching