[isabelle-dev] Fwd: isabelle test failed

Makarius makarius at sketis.net
Sat Jun 27 00:49:48 CEST 2015

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.


More information about the isabelle-dev mailing list