[isabelle-dev] Fwd: isabelle test failed
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 .
> 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
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