[isabelle-dev] NEWS: clarified 'case' command

[Makarius]

On Wed, 24 Jun 2015, Makarius wrote:

> After seeing too many "case 1", "case 2", "case 3" and corresponding 
> facts "1", "2", "3" I've now pushed this trivial change through, really 
> with rare incompatibilities.

Here is an example changeset that illustrates the reduction of odd digits 
and redundancy in the source, for better proof mainainability: 
http://isabelle.in.tum.de/repos/isabelle/rev/19c277ea65ae

I had already adapted these theories from HOL-Library and 
HOL-Decision_Procs earlier, to make use of 'consider' and statements with 
'if' / 'for'.  Thus raw proof blocks with big-bang integration by blast 
are mostly eliminated, and replaced by explicit proof structure.


 	Makarius