NEWS
changeset 19572 a4b3176f19dd
parent 19508 d5236f5b0a71
child 19587 eb063e7932d7
equal deleted inserted replaced
19571:0d673faf560c 19572:a4b3176f19dd
   397 "=" on type bool) are handled, variable names of the form "lit_<n>"
   397 "=" on type bool) are handled, variable names of the form "lit_<n>"
   398 are no longer reserved, significant speedup.
   398 are no longer reserved, significant speedup.
   399 
   399 
   400 * inductive and datatype: provide projections of mutual rules, bundled
   400 * inductive and datatype: provide projections of mutual rules, bundled
   401 as foo_bar.inducts;
   401 as foo_bar.inducts;
       
   402 
       
   403 * Library: theory Accessible_Part has been move to main HOL.
   402 
   404 
   403 * Library: added theory Coinductive_List of potentially infinite lists
   405 * Library: added theory Coinductive_List of potentially infinite lists
   404 as greatest fixed-point.
   406 as greatest fixed-point.
   405 
   407 
   406 * Library: added theory AssocList which implements (finite) maps as
   408 * Library: added theory AssocList which implements (finite) maps as