Re: [isabelle] Interpretation's fact hidden for unknown reason?
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 yahoo.fr> 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
> "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
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