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?



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