NEWS
changeset 73846 9447668d1b77
parent 73842 9134ae401ad5
child 73869 7181130f5872
equal deleted inserted replaced
73845:bfce186331be 73846:9447668d1b77
    99 (which is now also the default in "isabelle mkroot").
    99 (which is now also the default in "isabelle mkroot").
   100 
   100 
   101 * Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
   101 * Simplified typesetting of \<guillemotleft>...\<guillemotright> using \guillemotleft ...
   102 \guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
   102 \guillemotright from \usepackage[T1]{fontenc} --- \usepackage{babel} is
   103 no longer required.
   103 no longer required.
       
   104 
       
   105 
       
   106 *** Pure ***
       
   107 
       
   108 * "global_interpretation" is applicable in instantiation and overloading
       
   109 targets and in any nested target built on top of a target supporting
       
   110 "global_interpretation".
   104 
   111 
   105 
   112 
   106 *** HOL ***
   113 *** HOL ***
   107 
   114 
   108 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
   115 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,