contexts, locales, sym(metric);

fixing nat_combine_numerals simprocs (again) Theorem eq_cong2 moved from Integ/int_arith1.ML to simpdata.ML, where it will be available in all theories. Function simplify_meta_eq now makes the meta-equality first so that eq_cong2 will work properly.

enforce positive branch targets

fixed missing label

fixed document

tuned feedback of goal forms;

improved messages;

tuned local goal forms;

'declare': and_list1; 'obtain': updated;

tuned;