On Thu, 21 Nov 2013, Dmitriy Traytel wrote:
Issue1:
The theory is happily accepted by Isabelle/jEdit and Proof General, while the
build system chokes on it. The problem is the attempt to prove the theorem in
the wrong context.
However, I consider this a low precedence issue since it
* is discovered by the build system
* requires some Isabelle/ML
* occurs in Isabelle2013, Isabelle2013-1, and Isabelle/483131676087
Issue2 is perhaps slightly more severe:
With parallel proofs on this theory runs through (i.e. Isabelle/jEdit and
build are satisfied by default). With parallel proofs off one gets an
"unresolved flex-flex pair" (i.e. fails by default in Proof General). I'm not
sure if the parallel mode is smashing the pairs or simply ignoring them (I
hope the first).
Both of this is related to the old question how much structural integrity
the Goal.prove family of functions should enforce. Historically there
were many tools violating the basic context discipline, long before
"localization" emerged as a slogan, so it could not be too rigid.
I had checked the situation last time in 2009, so the current cfe53047dc16
to enforce more structure of goals was overdue. This avoids the flexflex
confusion of Issue2. The hyps problem behind Issue1 is still open,
because the Simplifier prems are not properly declared in the context, and
thus some simprocs that use them with Goal.prove would crash.
There is always something left in the continuous localization process ...
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
