NEWS
changeset 10756 831c864cc56e
parent 10726 e12b81140945
child 10770 4858ad0b8f38
equal deleted inserted replaced
10755:0fb476ff855c 10756:831c864cc56e
    76 operator;
    76 operator;
    77 
    77 
    78 * HOL/typedef: simplified package, provide more useful rules (see also
    78 * HOL/typedef: simplified package, provide more useful rules (see also
    79 HOL/subset.thy);
    79 HOL/subset.thy);
    80 
    80 
       
    81 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and 
       
    82 Fleuriot's mechanization of analysis;
       
    83 
       
    84 * HOL-Real, HOL-Hyperreals: improved arithmetic simplification;
    81 
    85 
    82 *** CTT ***
    86 *** CTT ***
    83 
    87 
    84 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
    88 * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that
    85 "lam" is displayed as TWO lambda-symbols
    89 "lam" is displayed as TWO lambda-symbols