[isabelle-dev] simplifier and subgoaler not transitive

[Makarius]

On Tue, 22 May 2012, Christian Urban wrote:

> Assuming that this is about the bowels of the simplifier,
> I hope this is the right place to ask the following question.

>From what I've seen on the thread so far, it is all perfectly normal 
Isabelle user-space.  You did not propose to re-implement the simplifier, 
so it could just as well be discussed on the larger audience of 
isabelle-users.  The experts are out there, and they are using Isabelle 
Professional Edition (aka release).


 	Makarius