NEWS
 changeset 4825 e4e56a1bcbe2 parent 4824 df8fc4626a9e child 4828 ee3317896a47
equal 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"`
`    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 `