Re: [isabelle] Theory merge in wrong order leads to error in datatype



Hi Dmitriy,

> 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.

a brief look through the history reveals the following change:

changeset:   63532:b01154b74314
user:        wenzelm
date:        Wed Jul 20 22:36:10 2016 +0200
summary:     provide Pure.simp/simp_all, which only know about
meta-equality;

I can see how that could create confusion with 'apply simp' (as the NEWS
entry indicats), but not how it could confuse internal tactics.

Cheers
Lars




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