[isabelle-dev] Advice for replacing @{simpset} with @{context}.

[Makarius]

On Thu, 12 Sep 2013, David Greenaway wrote:

> One of the changes that has occurred since Isabelle 2013 is that 
> simpsets have been deprecated in favour of storing simplifier rules 
> directly in the context.

"Deprecated" is is not really the wording we would use in the Isabelle 
context.  Sun/Oracle use that term for Java operations that are never 
changed, but Isabelle lives on continuous renovation for 25 years already.

The NEWS file explains what will happen in the coming release with simpset 
vs. Proof.context -- the Simplifier was one of the last hold-outs of 
non-localized tools, so after long delays we are mostly through with it.

Isabelle/jEdit has now this "Documentation" dockable to access 
documentation.  Its tree view also includes "NEWS" to access the 
all-important NEWS file with the "history user-relevant changes".  It also 
has its own jEdit editor mode with Sidekick tree etc. (The NEWS file still 
needs some polishing before we start the actual release candidate cycle in 
a few weeks.)


 	Makarius