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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
