NEWS
changeset 50126 3dec88149176
parent 50119 5c370a036de7
child 50132 180d086c30dd
equal deleted inserted replaced
50125:4319691be975 50126:3dec88149176
     3 
     3 
     4 New in this Isabelle version
     4 New in this Isabelle version
     5 ----------------------------
     5 ----------------------------
     6 
     6 
     7 *** General ***
     7 *** General ***
       
     8 
       
     9 * Theorem status about oracles and unfinished/failed future proofs is
       
    10 no longer printed by default, since it is incompatible with
       
    11 incremental / parallel checking of the persistent document model.  ML
       
    12 function Thm.peek_status may be used to inspect a snapshot of the
       
    13 ongoing evaluation process.  Note that in batch mode --- notably
       
    14 isabelle build --- the system ensures that future proofs of all
       
    15 accessible theorems in the theory context are finished (as before).
     8 
    16 
     9 * Configuration option show_markup controls direct inlining of markup
    17 * Configuration option show_markup controls direct inlining of markup
    10 into the printed representation of formal entities --- notably type
    18 into the printed representation of formal entities --- notably type
    11 and sort constraints.  This enables Prover IDE users to retrieve that
    19 and sort constraints.  This enables Prover IDE users to retrieve that
    12 information via tooltips in the output window, for example.
    20 information via tooltips in the output window, for example.