print_data moved to theory.ML; print_theory: exclude theorems (no forward reference!);

added THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq; added ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq; added EVERY: ('a -> 'a seq) list -> 'a -> 'a seq; added FIRST: ('a -> 'b seq) list -> 'a -> 'b seq; added TRY: ('a -> 'a seq) -> 'a -> 'a seq; added REPEAT: ('a -> 'a seq) -> 'a -> 'a seq;

added object.ML;

added option_map_o_empty added option_map_o_empty and option_map_o_update to simpset()

added split_etas

added split_sum_case_asm

tuned;

tuned msgs;

auto update

fixed ml_prompts;