[isabelle-dev] NEWS: clarified 'case' command
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