equal
deleted
inserted
replaced
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
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 |
|
11 |
|
12 *** Pure *** |
|
13 |
|
14 * Input syntax now supports dummy variable binding "%_. b", where the |
|
15 body does not mention the bound variable. Note that dummy patterns |
|
16 implicitly depend on their context of bounds, which makes "{_. _}" |
|
17 match any set comprehension as expected. |
|
18 |
|
19 * Removed obsolete syntactic constant _K and its associated parse |
|
20 translation. INCOMPATIBILITY, use dummy abstraction instead, for |
|
21 example "A -> B" => "Pi A (%_. B)". |
10 |
22 |
11 |
23 |
12 |
24 |
13 New in Isabelle2005 (October 2005) |
25 New in Isabelle2005 (October 2005) |
14 ---------------------------------- |
26 ---------------------------------- |