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

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


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