equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** HOL *** |
7 *** HOL *** |
|
8 |
|
9 * Dropped old infix syntax "mem" for List.member; use "in set" |
|
10 instead. INCOMPATIBILITY. |
|
11 |
|
12 * Refactoring of code-generation specific operations in List.thy |
|
13 |
|
14 constants |
|
15 null ~> List.null |
|
16 |
|
17 facts |
|
18 mem_iff ~> member_def |
|
19 null_empty ~> null_def |
|
20 |
|
21 INCOMPATIBILITY. Note that these were not suppossed to be used |
|
22 regularly unless for striking reasons; their main purpose was code |
|
23 generation. |
8 |
24 |
9 * Some previously unqualified names have been qualified: |
25 * Some previously unqualified names have been qualified: |
10 |
26 |
11 types |
27 types |
12 nat ~> Nat.nat |
28 nat ~> Nat.nat |