Re: [isabelle] Isabelle2016-1-RC3 available for testing: moreover then have

On 25/11/16 12:03, Christian Sternagel wrote:
> I use "moreover then have" a lot (mostly as the first "moreover"-step).
> But in the RC "then" is highlighted in red, which tells me that I
> shouldn't do this. Why?

Conceptually, Isar has a primary thread of facts called "this" and a
secondary one called "calculation". There are certain policies how
"this" vs. "calculation" are updated, going back to my PhD thesis,
various papers, and the official isar-ref manual.

At some point in history, there was an unfinished experiment that broke
this scheme. It was never documented and I have never seen better proofs
coming from it.

The red markup indicates such "improper Isar" that should be avoided if
you care about doing things properly.

Again, the update to Isar 2016 may be taken as an opportunity to brush
up old proof styles. It will lead to an overall improvement.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.