add restrict_space measure

better support for enat and ereal conversions

enat is countable

add equalities for SUP and INF over constant functions

add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image

add acyclicI_order

stronger inc_induct and dec_induct

countability of the image of a reflexive transitive closure

support of_rat with 0 or 1 on order relations

equation when indicator function equals 0 or 1

ported part of function package to new 'Ctr_Sugar' abstraction

undid copy-paste

ported 'partial_function' to 'Ctr_Sugar' abstraction

port list comprehension simproc to 'Ctr_Sugar' abstraction

added convenience function

document idiomatic use of 'simps_of_case'

ported 'Simps_Case_Conv' to use new 'Ctr_Sugar' abstraction

register old-style datatypes as 'Ctr_Sugar'

export useful ML function

moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it

tuned headers

moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction

updated sessions;

proper latex -- NB: cannot use antiquotation here;

merged

simplified App template;

obsolete;

obsolete;

tuned message;

tuned signature -- removed obsolete Addsimprocs, Delsimprocs;