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
interfaces.

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


	Makarius





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