NEWS
changeset 14606 0be6c11e7128
parent 14602 e06ded775eca
child 14610 9c2e31e483b2
equal deleted inserted replaced
14605:9de4d64eee3b 14606:0be6c11e7128
     1 Isabelle NEWS -- history user-relevant changes
     1 Isabelle NEWS -- history user-relevant changes
     2 ==============================================
     2 ==============================================
     3 
     3 
     4 New in this Isabelle release
     4 New in Isabelle2004 (April 2004)
     5 ----------------------------
     5 --------------------------------
     6 
     6 
     7 *** General ***
     7 *** General ***
     8 
     8 
     9 * Provers/order.ML:  new efficient reasoner for partial and linear orders.
     9 * Provers/order.ML:  new efficient reasoner for partial and linear orders.
    10   Replaces linorder.ML.
    10   Replaces linorder.ML.
    11 
    11 
    12 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
    12 * Pure: Greek letters (except small lambda, \<lambda>), as well as Gothic
    13   (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and euler
    13   (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and Euler
    14   (\<a>...\<z>), are now considered normal letters, and can therefore
    14   (\<a>...\<z>), are now considered normal letters, and can therefore
    15   be used anywhere where an ASCII letter (a...zA...Z) has until
    15   be used anywhere where an ASCII letter (a...zA...Z) has until
    16   now. COMPATIBILITY: This obviously changes the parsing of some
    16   now. COMPATIBILITY: This obviously changes the parsing of some
    17   terms, especially where a symbol has been used as a binder, say
    17   terms, especially where a symbol has been used as a binder, say
    18   '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed
    18   '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed
    21   existing theory and ML files.
    21   existing theory and ML files.
    22 
    22 
    23 * Pure: Macintosh and Windows line-breaks are now allowed in theory files.
    23 * Pure: Macintosh and Windows line-breaks are now allowed in theory files.
    24 
    24 
    25 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    25 * Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    26   allowed in identifiers. Similar to greek letters \<^isub> is now considered 
    26   allowed in identifiers. Similar to Greek letters \<^isub> is now considered 
    27   a normal (but invisible) letter. For multiple letter subscripts repeat 
    27   a normal (but invisible) letter. For multiple letter subscripts repeat 
    28   \<^isub> like this: x\<^isub>1\<^isub>2. 
    28   \<^isub> like this: x\<^isub>1\<^isub>2. 
    29 
    29 
    30 * Pure: There are now sub-/superscripts that can span more than one
    30 * Pure: There are now sub-/superscripts that can span more than one
    31   character. Text between \<^bsub> and \<^esub> is set in subscript in
    31   character. Text between \<^bsub> and \<^esub> is set in subscript in
    32   PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
    32   ProofGeneral and LaTeX, text between \<^bsup> and \<^esup> in
    33   new control characters are not identifier parts.
    33   superscript. The new control characters are not identifier parts.
    34 
    34 
    35 * Pure: Control-symbols of the form \<^raw:...> will literally print the
    35 * Pure: Control-symbols of the form \<^raw:...> will literally print the
    36   content of ... to the latex file instead of \isacntrl... . The ... 
    36   content of "..." to the latex file instead of \isacntrl... . The "..."
    37   accepts all printable characters excluding the end bracket >.
    37   may consist of any printable characters excluding the end bracket >.
    38 
    38 
    39 * Pure: Using new Isar command "finalconsts" (or the ML functions
    39 * Pure: Using new Isar command "finalconsts" (or the ML functions
    40   Theory.add_finals or Theory.add_finals_i) it is now possible to
    40   Theory.add_finals or Theory.add_finals_i) it is now possible to
    41   declare constants "final", which prevents their being given a definition
    41   declare constants "final", which prevents their being given a definition
    42   later.  It is useful for constants whose behaviour is fixed axiomatically
    42   later.  It is useful for constants whose behaviour is fixed axiomatically
    43   rather than definitionally, such as the meta-logic connectives.
    43   rather than definitionally, such as the meta-logic connectives.
    44 
    44 
    45 * Pure: It is now illegal to specify Theory.ML explicitly as a dependency
    45 * Pure: 'instance' now handles general arities with general sorts
    46   in the files section of the theory Theory. (This is more of a diagnostic
    46   (i.e. intersections of classes),
    47   than a restriction, as the theory loader screws up if Theory.ML is manually
       
    48   loaded.)
       
    49 
    47 
    50 * Presentation: generated HTML now uses a CSS style sheet to make layout
    48 * Presentation: generated HTML now uses a CSS style sheet to make layout
    51   (somewhat) independet of content. It is copied from lib/html/isabelle.css. 
    49   (somewhat) independent of content. It is copied from lib/html/isabelle.css. 
    52   It can be changed to alter the colors/layout of generated pages.
    50   It can be changed to alter the colors/layout of generated pages.
    53 
    51 
    54 
    52 
    55 *** Isar ***
    53 *** Isar ***
    56 
    54 
   170   formulae under an assignment of free variables to random values.
   168   formulae under an assignment of free variables to random values.
   171   In contrast to 'refute', it can deal with inductive datatypes,
   169   In contrast to 'refute', it can deal with inductive datatypes,
   172   but cannot handle quantifiers. See "HOL/ex/Quickcheck_Examples.thy"
   170   but cannot handle quantifiers. See "HOL/ex/Quickcheck_Examples.thy"
   173   for examples.
   171   for examples.
   174 
   172 
       
   173 
   175 *** HOLCF ***
   174 *** HOLCF ***
   176 
   175 
   177 * Streams now come with concatenation and are part of the HOLCF image
   176 * Streams now come with concatenation and are part of the HOLCF image
   178 
   177 
   179 
   178 
   180 
   179 
   181 New in Isabelle2003 (May 2003)
   180 New in Isabelle2003 (May 2003)
   182 --------------------------------
   181 ------------------------------
   183 
   182 
   184 *** General ***
   183 *** General ***
   185 
   184 
   186 * Provers/simplifier:
   185 * Provers/simplifier:
   187 
   186