equal
deleted
inserted
replaced
96 |
96 |
97 typ "_ * _ * bool * unit" :: finite |
97 typ "_ * _ * bool * unit" :: finite |
98 |
98 |
99 |
99 |
100 *** HOL *** |
100 *** HOL *** |
|
101 |
|
102 * Removed constant "chars". Prefer "Enum.enum" on type "char" |
|
103 directly. INCOMPATIBILITY. |
101 |
104 |
102 * Moved operation product, sublists and n_lists from Enum.thy |
105 * Moved operation product, sublists and n_lists from Enum.thy |
103 to List.thy. INCOMPATIBILITY. |
106 to List.thy. INCOMPATIBILITY. |
104 |
107 |
105 * Simplified 'typedef' specifications: historical options for implicit |
108 * Simplified 'typedef' specifications: historical options for implicit |