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