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.
a brief look through the history reveals the following change:
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