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