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

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)

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.


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