Re: [isabelle] Duplicate constant declaration in sublocale



Hi Andreas,

On 19.04.2013 12:27, Andreas Lochbihler wrote:
This looks really weird and I don't have an explanation, either, But you
can make B a sublocale of A if you move g's definition in A into the
locale declaration:

locale A = fixes G :: "('a, 'b) rec"
fixes g :: "'a => 'b => bool"
defines g_def: "g u e == proj G e = u"
begin
end

Thanks for your suggestion. Unfortunately, this is not an option for me as g is defined much later than the the locale.

  -- Lars




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