summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 02 Apr 2009 15:07:00 +0200 | |

changeset 30855 | c22436e6d350 |

parent 30854 | 740517878d60 |

child 30856 | 8b8d86cc2437 |

some more HOL-Nominal news;

--- a/NEWS Thu Apr 02 14:49:58 2009 +0200 +++ b/NEWS Thu Apr 02 15:07:00 2009 +0200 @@ -613,8 +613,36 @@ *** HOL-Nominal *** -* Modernized versions of commands 'nominal_inductive', -'nominal_primrec', and 'equivariance' work with local theory targets. +* Nominal datatypes can now contain type-variables. + +* Commands 'nominal_inductive' and 'equivariance' work with local +theory targets. + +* Nominal primrec can now works with local theory targets and its +specification syntax now conforms to the general format as seen in +'inductive' etc. + +* Method "perm_simp" honours the standard simplifier attributes +(no_asm), (no_asm_use) etc. + +* The new predicate #* is defined like freshness, except that on the +left hand side can be a set or list of atoms. + +* Experimental command 'nominal_inductive2' derives strong induction +principles for inductive definitions. In contrast to +'nominal_inductive', which can only deal with a fixed number of +binders, it can deal with arbitrary expressions standing for sets of +atoms to be avoided. The only inductive definition we have at the +moment that needs this generalisation is the typing rule for Lets in +the algorithm W: + + Gamma |- t1 : T1 (x,close Gamma T1)::Gamma |- t2 : T2 x#Gamma + ----------------------------------------------------------------- + Gamma |- Let x be t1 in t2 : T2 + +In this rule one wants to avoid all the binders that are introduced by +"close Gamma T1". We are looking for other examples where this +feature might be useful. Please let us know. *** HOLCF *** @@ -630,8 +658,8 @@ Potential INCOMPATIBILITY. * Command 'fixrec': specification syntax now conforms to the general -format as seen in 'inductive', 'primrec', 'function', etc. See -src/HOLCF/ex/Fixrec_ex.thy for examples. INCOMPATIBILITY. +format as seen in 'inductive' etc. See src/HOLCF/ex/Fixrec_ex.thy for +examples. INCOMPATIBILITY. *** ZF ***