NEWS
changeset 76043 b80f33e5323f
parent 76011 f56d239da777
child 76057 e07d873c18a4
child 76073 951abf9db857
equal deleted inserted replaced
76042:e076b1b42c44 76043:b80f33e5323f
    63 * Support for internal hyperlinks to files that belong formally to the
    63 * Support for internal hyperlinks to files that belong formally to the
    64 presented session.
    64 presented session.
    65 
    65 
    66 
    66 
    67 *** HOL ***
    67 *** HOL ***
       
    68 
       
    69 * HOL record: new simproc that sorts update expressions, guarded by
       
    70 configuration option "record_sort_updates" (default: false). Some
       
    71 examples are in theory "HOL-Examples.Records".
    68 
    72 
    69 * HOL-Algebra: Facts renamed to avoid fact name clashes on interpretation:
    73 * HOL-Algebra: Facts renamed to avoid fact name clashes on interpretation:
    70 
    74 
    71     is_ring ~> ring_axioms
    75     is_ring ~> ring_axioms
    72     cring ~> cring_axioms
    76     cring ~> cring_axioms