Re: [isabelle] Theory merge in wrong order leads to error in datatype
note that this is not specific to datatypes, but rather the general simplifier setup seems to be really messed up with this order of imports.
imports A Main
lemma "x = y â y = x"
by simp (* Failed to apply initial proof method *)
fun f where (*Tactic failed*)
"f x = x"
> On 13 Feb 2017, at 17:09, Lars Hupel <hupel at in.tum.de> wrote:
> Dear list,
> assume you have two files:
> theory A
> imports Pure
> begin (* empty *) end
> theory B
> imports A Main
> datatype 'a test = Test
> The "datatype" command produces a tactic failure, with the exception
> "Congruence not a meta-equality".
> If I swap the order of imports, the problem goes away.
> I'm aware that changing the order of imports might influence qualified
> names, but I haven't observed anything like that before. The above
> example throws an error in 2016-1 (and 49c537d87896), but succeeds in
This archive was generated by a fusion of
Pipermail (Mailman edition) and