NEWS
changeset 12245 3dd9aae402bb
parent 12210 2f510d8d8291
child 12253 1886dc96b7e9
equal deleted inserted replaced
12244:179f142ffb03 12245:3dd9aae402bb
   416 to "split_conv" (old name still available for compatibility);
   416 to "split_conv" (old name still available for compatibility);
   417 
   417 
   418 * HOL: improved concrete syntax for strings (e.g. allows translation
   418 * HOL: improved concrete syntax for strings (e.g. allows translation
   419 rules with string literals);
   419 rules with string literals);
   420 
   420 
   421 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals
   421 * HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals
   422 and Fleuriot's mechanization of analysis;
   422  and Fleuriot's mechanization of analysis, including the transcendental
       
   423  functions for the reals;
   423 
   424 
   424 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;
   425 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;
   425 
   426 
   426 
   427 
   427 *** CTT ***
   428 *** CTT ***