some more HOL-Nominal news;
authorwenzelm
Thu Apr 02 15:07:00 2009 +0200 (2009-04-02)
changeset 30855c22436e6d350
parent 30854 740517878d60
child 30856 8b8d86cc2437
some more HOL-Nominal news;
NEWS
     1.1 --- a/NEWS	Thu Apr 02 14:49:58 2009 +0200
     1.2 +++ b/NEWS	Thu Apr 02 15:07:00 2009 +0200
     1.3 @@ -613,8 +613,36 @@
     1.4  
     1.5  *** HOL-Nominal ***
     1.6  
     1.7 -* Modernized versions of commands 'nominal_inductive',
     1.8 -'nominal_primrec', and 'equivariance' work with local theory targets.
     1.9 +* Nominal datatypes can now contain type-variables.
    1.10 +
    1.11 +* Commands 'nominal_inductive' and 'equivariance' work with local
    1.12 +theory targets.
    1.13 +
    1.14 +* Nominal primrec can now works with local theory targets and its
    1.15 +specification syntax now conforms to the general format as seen in
    1.16 +'inductive' etc.
    1.17 +
    1.18 +* Method "perm_simp" honours the standard simplifier attributes
    1.19 +(no_asm), (no_asm_use) etc.
    1.20 +
    1.21 +* The new predicate #* is defined like freshness, except that on the
    1.22 +left hand side can be a set or list of atoms.
    1.23 +
    1.24 +* Experimental command 'nominal_inductive2' derives strong induction
    1.25 +principles for inductive definitions.  In contrast to
    1.26 +'nominal_inductive', which can only deal with a fixed number of
    1.27 +binders, it can deal with arbitrary expressions standing for sets of
    1.28 +atoms to be avoided.  The only inductive definition we have at the
    1.29 +moment that needs this generalisation is the typing rule for Lets in
    1.30 +the algorithm W:
    1.31 +
    1.32 + Gamma |- t1 : T1   (x,close Gamma T1)::Gamma |- t2 : T2   x#Gamma
    1.33 + -----------------------------------------------------------------
    1.34 +         Gamma |- Let x be t1 in t2 : T2
    1.35 +
    1.36 +In this rule one wants to avoid all the binders that are introduced by
    1.37 +"close Gamma T1".  We are looking for other examples where this
    1.38 +feature might be useful.  Please let us know.
    1.39  
    1.40  
    1.41  *** HOLCF ***
    1.42 @@ -630,8 +658,8 @@
    1.43  Potential INCOMPATIBILITY.
    1.44  
    1.45  * Command 'fixrec': specification syntax now conforms to the general
    1.46 -format as seen in 'inductive', 'primrec', 'function', etc.  See
    1.47 -src/HOLCF/ex/Fixrec_ex.thy for examples.  INCOMPATIBILITY.
    1.48 +format as seen in 'inductive' etc.  See src/HOLCF/ex/Fixrec_ex.thy for
    1.49 +examples.  INCOMPATIBILITY.
    1.50  
    1.51  
    1.52  *** ZF ***