equal
deleted
inserted
replaced
15 merely give a byte-oriented representation. |
15 merely give a byte-oriented representation. |
16 |
16 |
17 |
17 |
18 *** HOL *** |
18 *** HOL *** |
19 |
19 |
|
20 * Abolished symbol type names: "prod" and "sum" replace "*" and "+" |
|
21 respectively. INCOMPATBILITY. |
|
22 |
20 * Constant "split" has been merged with constant "prod_case"; names |
23 * Constant "split" has been merged with constant "prod_case"; names |
21 of ML functions, facts etc. involving split have been retained so far, |
24 of ML functions, facts etc. involving split have been retained so far, |
22 though. INCOMPATIBILITY. |
25 though. INCOMPATIBILITY. |
23 |
26 |
24 * Dropped old infix syntax "mem" for List.member; use "in set" |
27 * Dropped old infix syntax "mem" for List.member; use "in set" |
39 |
42 |
40 * Some previously unqualified names have been qualified: |
43 * Some previously unqualified names have been qualified: |
41 |
44 |
42 types |
45 types |
43 nat ~> Nat.nat |
46 nat ~> Nat.nat |
44 * ~> Product_Type.* |
|
45 + ~> Sum_Type.+ |
|
46 |
47 |
47 constants |
48 constants |
48 Ball ~> Set.Ball |
49 Ball ~> Set.Ball |
49 Bex ~> Set.Bex |
50 Bex ~> Set.Bex |
50 Suc ~> Nat.Suc |
51 Suc ~> Nat.Suc |
51 Pair ~> Product_Type.Pair |
52 Pair ~> Product_Type.Pair |
52 fst ~> Product_Type.fst |
53 fst ~> Product_Type.fst |
53 snd ~> Product_Type.snd |
54 snd ~> Product_Type.snd |
54 split ~> Product_Type.split |
|
55 curry ~> Product_Type.curry |
55 curry ~> Product_Type.curry |
|
56 op : ~> Set.member |
|
57 Collect ~> Set.Collect |
56 |
58 |
57 INCOMPATIBILITY. |
59 INCOMPATIBILITY. |
58 |
60 |
59 * Removed simplifier congruence rule of "prod_case", as has for long |
61 * Removed simplifier congruence rule of "prod_case", as has for long |
60 been the case with "split". |
62 been the case with "split". |