Re: [isabelle] new message

On Tue, 1 Nov 2005, Jeremy Dawson wrote:

> Using the current development version of Isabelle, I get a message
> ### Simplifier: no proof context in simpset -- fallback to theory context!

This means that you are using a simpset out-of-context, in which case the
Simplifier uses the theory context of the goal as fallback.  Apply
Simplifier.theory_context or Simplifier.context to provide an explicit
context yourself.  This is already done automatically by the system for
simpsets retrivied by simpset_of/local_simpset_of, which are the official

Important note: this information refers to the Isabelle development
version, which may change at any time without further notice.


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