NEWS
changeset 58202 be1d10595b7b
parent 58192 d0dffec0da2b
child 58247 98d0f85d247f
equal deleted inserted replaced
58201:5bf56c758e02 58202:be1d10595b7b
    11 
    11 
    12 * Command 'named_theorems' declares a dynamic fact within the context,
    12 * Command 'named_theorems' declares a dynamic fact within the context,
    13 together with an attribute to maintain the content incrementally.
    13 together with an attribute to maintain the content incrementally.
    14 This supersedes functor Named_Thms, but with a subtle change of
    14 This supersedes functor Named_Thms, but with a subtle change of
    15 semantics due to external visual order vs. internal reverse order.
    15 semantics due to external visual order vs. internal reverse order.
       
    16 
       
    17 
       
    18 *** Pure ***
       
    19 
       
    20 * Command "class_deps" takes optional sort arguments constraining
       
    21 the search space.
    16 
    22 
    17 
    23 
    18 *** HOL ***
    24 *** HOL ***
    19 
    25 
    20 * Command and antiquotation "value" provide different evaluation slots (again),
    26 * Command and antiquotation "value" provide different evaluation slots (again),