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

Makarius makarius at sketis.net
Thu Jun 25 00:30:21 CEST 2015

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: 

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.


More information about the isabelle-dev mailing list