NEWS
changeset 4825 e4e56a1bcbe2
parent 4824 df8fc4626a9e
child 4828 ee3317896a47
equal deleted inserted replaced
4824:df8fc4626a9e 4825:e4e56a1bcbe2
    38   which means that !!-bound variables are splitted much more aggressively.
    38   which means that !!-bound variables are splitted much more aggressively.
    39   If this splitting is not appropriate, use delSWrapper "split_all_tac".
    39   If this splitting is not appropriate, use delSWrapper "split_all_tac".
    40 
    40 
    41 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
    41 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
    42 
    42 
    43 * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized
    43 * HOL/Arithmetic
    44   some theorems about n-1
    44   
       
    45   - removed 'pred' (predecessor) function
       
    46 
       
    47   - generalized some theorems about n-1
       
    48 
       
    49   - Many new laws about "div" and "mod"
       
    50 
       
    51   - New laws about greatest common divisors (see theory ex/Primes)
    45 
    52 
    46 * HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of
    53 * HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of
    47   "inverse"
    54   "inverse"
    48 
       
    49 * HOL/equalities: added many new laws involving unions, intersectinos,
       
    50   difference, etc.
       
    51 
    55 
    52 * recdef can now declare non-recursive functions, with {} supplied as the 
    56 * recdef can now declare non-recursive functions, with {} supplied as the 
    53   well-founded relation
    57   well-founded relation
    54 
    58 
    55 * Simplifier:
    59 * Simplifier:
    72   For compatibility reasons there is now Asm_lr_simp_tac which is like the
    76   For compatibility reasons there is now Asm_lr_simp_tac which is like the
    73   old Asm_full_simp_tac in that it does not rotate premises.
    77   old Asm_full_simp_tac in that it does not rotate premises.
    74 
    78 
    75 * new theory Vimage (inverse image of a function, syntax f-``B);
    79 * new theory Vimage (inverse image of a function, syntax f-``B);
    76 
    80 
    77 * many new identities for unions, intersections, etc.;
    81 * many new identities for unions, intersections, set difference, etc.;
    78 
    82 
    79 
    83 
    80 New in Isabelle98 (January 1998)
    84 New in Isabelle98 (January 1998)
    81 --------------------------------
    85 --------------------------------
    82 
    86