NEWS
 changeset 17865 5b0c3dcfbad2 parent 17809 195045659c06 child 17869 585c1f08499e
equal inserted replaced
17864:b039ea8bb965 17865:5b0c3dcfbad2
`     7 *** General ***`
`     7 *** General ***`
`     8 `
`     8 `
`     9 * Command 'find_theorems': support "*" wildcard in "name:" criterion.`
`     9 * Command 'find_theorems': support "*" wildcard in "name:" criterion.`
`    10 `
`    10 `
`    11 `
`    11 `
`       `
`    12 *** Document preparation ***`
`       `
`    13 `
`       `
`    14 * Added antiquotations @{ML_type text} and @{ML_struct} which check`
`       `
`    15 the given source text as ML type/structure, printing verbatim.`
`       `
`    16 `
`       `
`    17 `
`    12 *** Pure ***`
`    18 *** Pure ***`
`       `
`    19 `
`       `
`    20 * Isar: improper proof element 'guess' is like 'obtain', but derives`
`       `
`    21 the obtained context from the course of reasoning!  For example:`
`       `
`    22 `
`       `
`    23   assume "EX x y. A x & B y"   -- "any previous fact"`
`       `
`    24   then guess x and y by clarify`
`       `
`    25 `
`       `
`    26 This technique is potentially adventurous, depending on the facts and`
`       `
`    27 proof tools being involved here.`
`    13 `
`    28 `
`    14 * Input syntax now supports dummy variable binding "%_. b", where the`
`    29 * Input syntax now supports dummy variable binding "%_. b", where the`
`    15 body does not mention the bound variable.  Note that dummy patterns`
`    30 body does not mention the bound variable.  Note that dummy patterns`
`    16 implicitly depend on their context of bounds, which makes "{_. _}"`
`    31 implicitly depend on their context of bounds, which makes "{_. _}"`
`    17 match any set comprehension as expected.  Potential INCOMPATIBILITY --`
`    32 match any set comprehension as expected.  Potential INCOMPATIBILITY --`
`    20 `
`    35 `
`    21 * Removed obsolete syntactic constant "_K" and its associated parse`
`    36 * Removed obsolete syntactic constant "_K" and its associated parse`
`    22 translation.  INCOMPATIBILITY -- use dummy abstraction instead, for`
`    37 translation.  INCOMPATIBILITY -- use dummy abstraction instead, for`
`    23 example "A -> B" => "Pi A (%_. B)".`
`    38 example "A -> B" => "Pi A (%_. B)".`
`    24 `
`    39 `
`       `
`    40 `
`    25 *** HOL ***`
`    41 *** HOL ***`
`    26 `
`    42 `
`    27 * In the context of the assumption "~(s = t)" the simplifier rewrites`
`    43 * In the context of the assumption "~(s = t)" the Simplifier rewrites`
`    28 "t = s" to False (by simproc "neq_simproc"). For backward compatibility`
`    44 "t = s" to False (by simproc "neq_simproc").  For backward`
`    29 this can be disabled by ML"reset use_neq_simproc".`
`    45 compatibility this can be disabled by ML "reset use_neq_simproc".`
`    30 `
`    46 `
`    31 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals`
`    47 * Tactics 'sat' and 'satx' reimplemented, several improvements: goals`
`    32 no longer need to be stated as "<prems> ==> False", equivalences (i.e.`
`    48 no longer need to be stated as "<prems> ==> False", equivalences (i.e.`
`    33 "=" on type bool) are handled, variable names of the form "lit_<n>" are`
`    49 "=" on type bool) are handled, variable names of the form "lit_<n>"`
`    34 no longer reserved, significant speedup.`
`    50 are no longer reserved, significant speedup.`
`       `
`    51 `
`    35 `
`    52 `
`    36 `
`    53 `
`    37 New in Isabelle2005 (October 2005)`
`    54 New in Isabelle2005 (October 2005)`
`    38 ----------------------------------`
`    55 ----------------------------------`
`    39 `
`    56 `