tuned Nominal entry;
authorwenzelm
Mon Oct 22 21:32:06 2007 +0200 (2007-10-22)
changeset 251489c9646c1080d
parent 25147 85463aff6dbe
child 25149 776f985efa4c
tuned Nominal entry;
ANNOUNCE
NEWS
     1.1 --- a/ANNOUNCE	Mon Oct 22 16:54:54 2007 +0200
     1.2 +++ b/ANNOUNCE	Mon Oct 22 21:32:06 2007 +0200
     1.3 @@ -11,8 +11,8 @@
     1.4  
     1.5  The main highlights are:
     1.6  
     1.7 -* Fully featured support for nominal datatypes (binding structures)
     1.8 -due to the HOL-Nominal logic.
     1.9 +* Support for nominal datatypes (binding structures) due to the
    1.10 +HOL-Nominal logic.
    1.11  
    1.12  * General local theory infrastructure for specifications depending on
    1.13  parameters and assumptions (e.g. from locales, classes).
     2.1 --- a/NEWS	Mon Oct 22 16:54:54 2007 +0200
     2.2 +++ b/NEWS	Mon Oct 22 21:32:06 2007 +0200
     2.3 @@ -1200,14 +1200,11 @@
     2.4  
     2.5  *** HOL-Nominal ***
     2.6  
     2.7 -* Not yet complete support for nominal datatypes (binding structures)
     2.8 -based on HOL-Nominal logic. See HOL/Nominal and HOL/Nominal/Examples.
     2.9 -If you plan to use nominal datatypes you are strongly advised to
    2.10 -visit 
    2.11 -
    2.12 - http://isabelle.in.tum.de/nominal/
    2.13 -
    2.14 -and look there for up-to-date information.
    2.15 +* Substantial, yet incomplete support for nominal datatypes (binding
    2.16 +structures) based on HOL-Nominal logic.  See HOL/Nominal and
    2.17 +HOL/Nominal/Examples.  Prespective users should consult
    2.18 +http://isabelle.in.tum.de/nominal/
    2.19 +
    2.20  
    2.21  *** ML ***
    2.22