NEWS
changeset 2654 6efa602921d1
parent 2653 f1a6997cdc06
child 2705 d6e83a02061d
equal deleted inserted replaced
2653:f1a6997cdc06 2654:6efa602921d1
     1 
     1 
     2 Isabelle NEWS -- history of user-visible changes
     2 Isabelle NEWS -- history of user-visible changes
     3 ================================================
     3 ================================================
     4 
     4 
     5 New in Isabelle94-8 (??????????? 1997 FIXME)
     5 New in Isabelle94-8 (really-soon-now 1997 FIXME)
     6 ---------------------------------------
     6 ------------------------------------------------
       
     7 
     7 * HOLCF changes: derived all rules and arities 
     8 * HOLCF changes: derived all rules and arities 
     8   + axiomatic type classes instead of classes 
     9   + axiomatic type classes instead of classes 
     9   + typedef instead of faking type definitions
    10   + typedef instead of faking type definitions
    10   + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
    11   + eliminated the initernal constants less_fun, less_cfun, UU_fun, UU_cfun etc.
    11   + new axclasses cpo,chfin,flat with flat<chfin<pcpo<cpo<po
    12   + new axclasses cpo,chfin,flat with flat<chfin<pcpo<cpo<po
    68 
    69 
    69 * more default rewrite rules in HOL for quantifiers, union/intersection;
    70 * more default rewrite rules in HOL for quantifiers, union/intersection;
    70 
    71 
    71 * the NEWS file;
    72 * the NEWS file;
    72 
    73 
    73 Changes in HOLCF:
       
    74 
       
    75 
    74 
    76 New in Isabelle94-7 (November 96)
    75 New in Isabelle94-7 (November 96)
    77 ---------------------------------
    76 ---------------------------------
    78 
    77 
    79 * allowing negative levels (as offsets) in prlev and choplev;
    78 * allowing negative levels (as offsets) in prlev and choplev;