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



On 14/02/17 08:18, Dmitriy Traytel wrote:
> 
> 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.

This is correct. Theories cannot be merged in arbitrary ways, especially
not bootstrap theories.

In this particular case, the problem is the Simplifier setup: it changes
a few times, until it somehow stabilizes within HOL. The datails are
subject to change over the years.

Problems are to be expected, when applications do anything below theory
Main (or Complex_Main), which are the only official entry points of
Isabelle/HOL.


	Makarius





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