equal
deleted
inserted
replaced
67 |
67 |
68 typ "_ * _ * bool * unit" :: finite |
68 typ "_ * _ * bool * unit" :: finite |
69 |
69 |
70 |
70 |
71 *** HOL *** |
71 *** HOL *** |
|
72 |
|
73 * Moved operation product, sublists and n_lists from Enum.thy |
|
74 to List.thy. INCOMPATIBILITY. |
72 |
75 |
73 * Simplified 'typedef' specifications: historical options for implicit |
76 * Simplified 'typedef' specifications: historical options for implicit |
74 set definition and alternative name have been discontinued. The |
77 set definition and alternative name have been discontinued. The |
75 former behavior of "typedef (open) t = A" is now the default, but |
78 former behavior of "typedef (open) t = A" is now the default, but |
76 written just "typedef t = A". INCOMPATIBILITY, need to adapt theories |
79 written just "typedef t = A". INCOMPATIBILITY, need to adapt theories |