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

Hi Yannick,

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 and
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> wrote:

> 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

Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

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