NEWS
changeset 33627 ffb4a811e34d
parent 33524 a08e6c1cbc04
child 33639 603320b93668
equal deleted inserted replaced
33626:42f69386943a 33627:ffb4a811e34d
    34 (old form is still retained for backward compatibility).
    34 (old form is still retained for backward compatibility).
    35 Styles can be also applied for antiquotations prop, term_type and typeof.
    35 Styles can be also applied for antiquotations prop, term_type and typeof.
    36 
    36 
    37 
    37 
    38 *** HOL ***
    38 *** HOL ***
       
    39 
       
    40 * New commands "code_pred" and "values" to invoke the predicate compiler
       
    41 and to enumerate values of inductive predicates.
    39 
    42 
    40 * Combined former theories Divides and IntDiv to one theory Divides
    43 * Combined former theories Divides and IntDiv to one theory Divides
    41 in the spirit of other number theory theories in HOL;  some constants
    44 in the spirit of other number theory theories in HOL;  some constants
    42 (and to a lesser extent also facts) have been suffixed with _nat und _int
    45 (and to a lesser extent also facts) have been suffixed with _nat und _int
    43 respectively.  INCOMPATIBILITY.
    46 respectively.  INCOMPATIBILITY.