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



Dear Makarius,

Makarius wrote:
> 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.

None of the above (nor the remainder of your email) explains what is
wrong with "moreover then have". As I understand it, "moreover" updates
the calculation, and "then" chains the same fact into the next goal.
This is useful. Which principle is violated here?

Cheers,

Bertram




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