removed duplicate lemma

derive (co)rec uniformly from (un)fold

NEWS;

updated documentation;

more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;

unused (see caaa2fc4040d);

simplified default print_depth: context is usually available, in contrast to 0d295e339f52;

clarified bootstrap of @{make_string} -- avoid query on ML environment;