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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
