Re: [isabelle] Duplicate constant declaration in sublocale
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 A = fixes G :: "('a, 'b) rec"
fixes g :: "'a => 'b => bool"
defines g_def: "g u e == proj G e = u"
Thanks for your suggestion. Unfortunately, this is not an option for me
as g is defined much later than the the locale.
This archive was generated by a fusion of
Pipermail (Mailman edition) and