Re: [isabelle] Interpretation's fact hidden for unknown reason?
Le Wed, 06 Feb 2013 20:22:01 +0100, Yannick
<yannick_duchene at yahoo.fr> a écrit:
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).
I just tried this, base on the same sample case:
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)
As‑is, I1.P and I2.P are both visible, but still cannot see both at the
same time. If in theory “TI2”, I change “imports TL” into “imports TI1”,
then the same issue occurs, “I2.P” is not visible.
Using separate theories allows to have both, but still not simultaneously.
“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