NEWS
changeset 24032 b3d7eb6f535f
parent 23977 5a3ec03c825b
child 24086 21900a460ba4
     1.1 --- a/NEWS	Sat Jul 28 22:01:06 2007 +0200
     1.2 +++ b/NEWS	Sat Jul 28 22:17:46 2007 +0200
     1.3 @@ -161,6 +161,24 @@
     1.4  Command 'print_theory' outputs the normalized system of recursive
     1.5  equations, see section "definitions".
     1.6  
     1.7 +* Isar: command 'declaration' augments a local theory by generic
     1.8 +declaration functions written in ML.  This enables arbitrary content
     1.9 +being added to the context, depending on a morphism that tells the
    1.10 +difference of the original declaration context wrt. the application
    1.11 +context encountered later on.
    1.12 +
    1.13 +* Isar: proper interfaces for simplification procedures.  Command
    1.14 +'simproc_setup' declares named simprocs (with match patterns, and body
    1.15 +text in ML).  Attribute "simproc" adds/deletes simprocs in the current
    1.16 +context.  ML antiquotation @{simproc name} retrieves named simprocs.
    1.17 +
    1.18 +* Isar: an extra pair of brackets around attribute declarations
    1.19 +abbreviates a theorem reference involving an internal dummy fact,
    1.20 +which will be ignored later --- only the effect of the attribute on
    1.21 +the background context will persist.  This form of in-place
    1.22 +declarations is particularly useful with commands like 'declare' and
    1.23 +'using', for example ``have A using [[simproc a]] by simp''.
    1.24 +
    1.25  * Isar: method "assumption" (and implicit closing of subproofs) now
    1.26  takes simple non-atomic goal assumptions into account: after applying
    1.27  an assumption as a rule the resulting subgoals are solved by atomic