NEWS
changeset 76057 e07d873c18a4
parent 76056 c2fd8b88d262
parent 76043 b80f33e5323f
child 76093 ce66ff654e59
equal deleted inserted replaced
76056:c2fd8b88d262 76057:e07d873c18a4
    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