NEWS
changeset 21960 0574f192b78a
parent 21896 9a7949815a84
child 22125 cc35c948f6c5
equal deleted inserted replaced
21959:b50182aff75f 21960:0574f192b78a
    39 ``context/locale/class ... begin'' followed by ``end''.  The body may
    39 ``context/locale/class ... begin'' followed by ``end''.  The body may
    40 contain definitions, theorems etc., including any derived mechanism
    40 contain definitions, theorems etc., including any derived mechanism
    41 that has been implemented on top of these primitives.  This concept
    41 that has been implemented on top of these primitives.  This concept
    42 generalizes the existing ``theorem (in ...)'' towards more versatility
    42 generalizes the existing ``theorem (in ...)'' towards more versatility
    43 and scalability.
    43 and scalability.
       
    44 
       
    45 * Proof General interface: proper undo of final 'end' command;
       
    46 discontinued Isabelle/classic mode (ML proof scripts).
    44 
    47 
    45 
    48 
    46 *** Document preparation ***
    49 *** Document preparation ***
    47 
    50 
    48 * Added antiquotation @{theory name} which prints the given name,
    51 * Added antiquotation @{theory name} which prints the given name,