[isabelle] Interpretation's fact hidden for unknown reason?
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
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and