Make a couple of important termination theorems automatic rewrites.

In particular:

   |- WF $<
   |- inv_image R f x y <=> R (f x) (f y)
Rename implicational theorems in relation to make room for equivalences

This affects TC_CASES1 and TC_CASES2 that were hardly ever being used.
See the release notes change for more discussion.
Slight clarification of language about Datatype in release notes.
Minor reformatting in release notes
A bunch of new theorems in bagTheory; mostly about the multiset order.
A new failing test-case for the arithmetic d.p.