Re: [isabelle] sublocale problem



Le 14/10/2015 08:20, Andreas Lochbihler a Ãcrit :
Dear Esseger,

1. Interpretations can be given name prefixes to avoid clashes. For
example,

interpretation prefix!: AAA M2 T2

That's exactly what I need, thanks a lot.


2. Unfortunately, the sublocale command does not export the rule for
showing the locale predicate of superlocales. Consequently, I recommend
to first prove sublocale proof obligation in a lemma and then use the
lemma for discharging the goal in the sublocale command. Here's an example:

context AAA begin
lemma BBB: "BBB M T" <proof>
sublocale BBB M T by(rule BBB)
end

This is what I was doing, but it was getting tedious as in my use case there is a chain of inclusions, so having a lemma for each inclusion was really not convenient.

Best,
Esseger







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