NEWS
changeset 56499 7e0178c84994
parent 56450 16d4213d4cbc
child 56505 aed94b61f65b
equal deleted inserted replaced
56498:6437c989a744 56499:7e0178c84994
    22 
    22 
    23 * Lexical syntax (inner and outer) supports text cartouches with
    23 * Lexical syntax (inner and outer) supports text cartouches with
    24 arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
    24 arbitrary nesting, and without escapes of quotes etc.  The Prover IDE
    25 supports input methods via ` (backquote), or << and >> (double angle
    25 supports input methods via ` (backquote), or << and >> (double angle
    26 brackets).
    26 brackets).
       
    27 
       
    28 * The outer syntax categories "text" (for formal comments and document
       
    29 markup commands) and "altstring" (for literal fact references) allow
       
    30 cartouches as well, in addition to the traditional mix of quotations.
    27 
    31 
    28 * More static checking of proof methods, which allows the system to
    32 * More static checking of proof methods, which allows the system to
    29 form a closure over the concrete syntax.  Method arguments should be
    33 form a closure over the concrete syntax.  Method arguments should be
    30 processed in the original proof context as far as possible, before
    34 processed in the original proof context as far as possible, before
    31 operating on the goal state.  In any case, the standard discipline for
    35 operating on the goal state.  In any case, the standard discipline for