# HG changeset patch
# User wenzelm
# Date 1185653866 -7200
# Node ID b3d7eb6f535f09595d79679ee1f44e301b50309a
# Parent  e94e541346d7a24c85c9051d3b9dbd2d86954b96
* Isar: command 'declaration';
* Isar: proper interfaces for simplification procedures;
* Isar: an extra pair of brackets around attribute declarations
  abbreviates a theorem reference involving an internal dummy fact;

diff -r e94e541346d7 -r b3d7eb6f535f NEWS
--- a/NEWS	Sat Jul 28 22:01:06 2007 +0200
+++ b/NEWS	Sat Jul 28 22:17:46 2007 +0200
@@ -161,6 +161,24 @@
 Command 'print_theory' outputs the normalized system of recursive
 equations, see section "definitions".
 
+* Isar: command 'declaration' augments a local theory by generic
+declaration functions written in ML.  This enables arbitrary content
+being added to the context, depending on a morphism that tells the
+difference of the original declaration context wrt. the application
+context encountered later on.
+
+* Isar: proper interfaces for simplification procedures.  Command
+'simproc_setup' declares named simprocs (with match patterns, and body
+text in ML).  Attribute "simproc" adds/deletes simprocs in the current
+context.  ML antiquotation @{simproc name} retrieves named simprocs.
+
+* Isar: an extra pair of brackets around attribute declarations
+abbreviates a theorem reference involving an internal dummy fact,
+which will be ignored later --- only the effect of the attribute on
+the background context will persist.  This form of in-place
+declarations is particularly useful with commands like 'declare' and
+'using', for example ``have A using [[simproc a]] by simp''.
+
 * Isar: method "assumption" (and implicit closing of subproofs) now
 takes simple non-atomic goal assumptions into account: after applying
 an assumption as a rule the resulting subgoals are solved by atomic