[isabelle-dev] Fwd: isabelle test failed

[Makarius]

On Sat, 27 Jun 2015, Dmitriy Traytel wrote:

> Oops, I didn't expect my name to appear here ;-)
>
> The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report [1]. 
> With turned off proofs the effect was a good one.
>
> What is special about Pure.conjunction w.r.t. proof reconstruction? Is it 
> something in Goal.conjunction_tac? Would you advise to use HOL's conjunction 
> instead?

I don't know if there is a difference between Pure and HOL.  We could ask 
Stefan Berghofer, or just check empirically.

The question arose first in 2007/2008 when Alex Krauss introduced many 
multi-goals in the function package.  I can't say on the spot if/how that 
was addressed, or rather worked-around.


 	Makarius