Re: [isabelle] Interpretation's fact hidden for unknown reason?
One may also not only enjoy different proofs, but need different proofs.
May be a workaround is to move each interpretation in its own theory file,
but that may lead to other issues (I did not try).
We will have to wait to know if it's on purpose or not.
On Wed, 06 Feb 2013 12:39:17 +0100, Alfio Martini <alfio.martini at acm.org>
I have also the same doubt with respect to the same situation. In a
more complex setting, I usually
like to try several different proofs for the same locale interpretation
because of the situation mentioned below I find that I can not do it.
On Wed, Feb 6, 2013 at 1:37 AM, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> wrote:
I don't understand why in the following (simple and stupid) sample
case, the P fact from the second interpretation, is >>not visible:
locale L = fixes A assumes P: "A = A"
interpretation I1: L A by (unfold L_def, rule refl)
interpretation I2: L A by (unfold L_def, rule refl)
At “thm I2.P” the ouput pan says “Unknown fact I2.P”. If I move I2
before I1, then I2.P becomes visible and I1.P is >>hidden.
Note: it occurs with Isabelle RC2.
Is this normal behaviour? If yes, then I must be miss‑understanding
This archive was generated by a fusion of
Pipermail (Mailman edition) and