Pure: 'instance' now handles general arities;
authorwenzelm
Fri Apr 16 21:00:07 2004 +0200 (2004-04-16)
changeset 146060be6c11e7128
parent 14605 9de4d64eee3b
child 14607 099575a938e5
Pure: 'instance' now handles general arities;
NEWS
     1.1 --- a/NEWS	Fri Apr 16 20:59:09 2004 +0200
     1.2 +++ b/NEWS	Fri Apr 16 21:00:07 2004 +0200
     1.3 @@ -1,16 +1,16 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 -New in this Isabelle release
     1.8 -----------------------------
     1.9 +New in Isabelle2004 (April 2004)
    1.10 +--------------------------------
    1.11  
    1.12  *** General ***
    1.13  
    1.14  * Provers/order.ML:  new efficient reasoner for partial and linear orders.
    1.15    Replaces linorder.ML.
    1.16  
    1.17 -* Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
    1.18 -  (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and euler
    1.19 +* Pure: Greek letters (except small lambda, \<lambda>), as well as Gothic
    1.20 +  (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and Euler
    1.21    (\<a>...\<z>), are now considered normal letters, and can therefore
    1.22    be used anywhere where an ASCII letter (a...zA...Z) has until
    1.23    now. COMPATIBILITY: This obviously changes the parsing of some
    1.24 @@ -23,18 +23,18 @@
    1.25  * Pure: Macintosh and Windows line-breaks are now allowed in theory files.
    1.26  
    1.27  * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    1.28 -  allowed in identifiers. Similar to greek letters \<^isub> is now considered 
    1.29 +  allowed in identifiers. Similar to Greek letters \<^isub> is now considered 
    1.30    a normal (but invisible) letter. For multiple letter subscripts repeat 
    1.31    \<^isub> like this: x\<^isub>1\<^isub>2. 
    1.32  
    1.33  * Pure: There are now sub-/superscripts that can span more than one
    1.34    character. Text between \<^bsub> and \<^esub> is set in subscript in
    1.35 -  PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
    1.36 -  new control characters are not identifier parts.
    1.37 +  ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in
    1.38 +  superscript. The new control characters are not identifier parts.
    1.39  
    1.40  * Pure: Control-symbols of the form \<^raw:...> will literally print the
    1.41 -  content of ... to the latex file instead of \isacntrl... . The ... 
    1.42 -  accepts all printable characters excluding the end bracket >.
    1.43 +  content of "..." to the latex file instead of \isacntrl... . The "..."
    1.44 +  may consist of any printable characters excluding the end bracket >.
    1.45  
    1.46  * Pure: Using new Isar command "finalconsts" (or the ML functions
    1.47    Theory.add_finals or Theory.add_finals_i) it is now possible to
    1.48 @@ -42,13 +42,11 @@
    1.49    later.  It is useful for constants whose behaviour is fixed axiomatically
    1.50    rather than definitionally, such as the meta-logic connectives.
    1.51  
    1.52 -* Pure: It is now illegal to specify Theory.ML explicitly as a dependency
    1.53 -  in the files section of the theory Theory. (This is more of a diagnostic
    1.54 -  than a restriction, as the theory loader screws up if Theory.ML is manually
    1.55 -  loaded.)
    1.56 +* Pure: 'instance' now handles general arities with general sorts
    1.57 +  (i.e. intersections of classes),
    1.58  
    1.59  * Presentation: generated HTML now uses a CSS style sheet to make layout
    1.60 -  (somewhat) independet of content. It is copied from lib/html/isabelle.css. 
    1.61 +  (somewhat) independent of content. It is copied from lib/html/isabelle.css. 
    1.62    It can be changed to alter the colors/layout of generated pages.
    1.63  
    1.64  
    1.65 @@ -172,6 +170,7 @@
    1.66    but cannot handle quantifiers. See "HOL/ex/Quickcheck_Examples.thy"
    1.67    for examples.
    1.68  
    1.69 +
    1.70  *** HOLCF ***
    1.71  
    1.72  * Streams now come with concatenation and are part of the HOLCF image
    1.73 @@ -179,7 +178,7 @@
    1.74  
    1.75  
    1.76  New in Isabelle2003 (May 2003)
    1.77 ---------------------------------
    1.78 +------------------------------
    1.79  
    1.80  *** General ***
    1.81