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

Le Wed, 06 Feb 2013 20:22:01 +0100, Yannick <yannick_duchene at> 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:

    theory TL
    imports HOL
      locale L = fixes A assumes P: "A = A"
      thm L.P

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

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

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.” [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.