On Mon, 3 Dec 2012, Jasmin Christian Blanchette wrote:
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
~~/src/HOL/Proofs/Lambda/StrongNorm
begin
On Mon, 3 Dec 2012, Lawrence Paulson wrote:
Surely the existence of two theories of the same name can be detected?
The deeper problem here is that theories still have the ancient flat name
space. So the file-system paths in the source are ultimately stripped to
the base name when doing
Am 08.12.2012 um 14:07 schrieb Makarius:
In your observations above, are you sure that nondeterministically means
physical nondeterminism, say due to parallel loading of theories? Or
theories that you have visited before in Proof General, before starting the
above one?
Each time I
Of course a full solution might be a lot of work. But merely to detect the
presence of two identically-named theories (in the spirit of detecting
instances of a variable with two different types) might be straightforward,
even if the only response is a fatal error. Since otherwise the outcome
Hi all,
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
~~/src/HOL/Proofs/Lambda/StrongNorm
begin
nondeterministically gives either
***
Am 03.12.2012 um 22:31 schrieb Jasmin Christian Blanchette:
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe
~~/src/HOL/Proofs/Lambda/StrongNorm
Am 03.12.2012 um 23:08 schrieb Lawrence Paulson:
Missing components maybe?
I did isabelle components -a earlier today. In fact, the issue is likely to
be related to the big upgrade that resulted from my invocation of this very
command yesterday night.
Jasmin
Did you try starting jEdit with -f to force a fresh build?
Jasmin Blanchette jasmin.blanche...@gmail.com schrieb:
Am 03.12.2012 um 23:08 schrieb Lawrence Paulson:
Missing components maybe?
I did isabelle components -a earlier today. In fact, the issue is likely to
be related to the big
Am 04.12.2012 um 07:51 schrieb Lars Noschinski:
Did you try starting jEdit with -f to force a fresh build?
That did the trick. Thanks!
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
