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 |