[isabelle] Interpretation's fact hidden for unknown reason?



Hi all,

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"
    thm L.P

    interpretation I1: L A by (unfold L_def, rule refl)
    thm I1.P

    interpretation I2: L A by (unfold L_def, rule refl)
    thm I2.P


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 something.


--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.