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:

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

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

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

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.