equal
deleted
inserted
replaced
38 situations. |
38 situations. |
39 |
39 |
40 |
40 |
41 *** HOL *** |
41 *** HOL *** |
42 |
42 |
|
43 * Library/Option_ord.thy: Canonical order on option type. |
|
44 |
43 * Library/RBT.thy: New theory of red-black trees, an efficient |
45 * Library/RBT.thy: New theory of red-black trees, an efficient |
44 implementation of finite maps. |
46 implementation of finite maps. |
|
47 |
|
48 * Library/Countable.thy: Type class for countable types. |
45 |
49 |
46 * Theory Int: The representation of numerals has changed. The infix |
50 * Theory Int: The representation of numerals has changed. The infix |
47 operator BIT and the bit datatype with constructors B0 and B1 have |
51 operator BIT and the bit datatype with constructors B0 and B1 have |
48 disappeared. INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in |
52 disappeared. INCOMPATIBILITY, use "Int.Bit0 x" and "Int.Bit1 y" in |
49 place of "x BIT bit.B0" and "y BIT bit.B1", respectively. Theorems |
53 place of "x BIT bit.B0" and "y BIT bit.B1", respectively. Theorems |
5241 |
5245 |
5242 * 'subtype' facility in HOL for introducing new types as subsets of existing |
5246 * 'subtype' facility in HOL for introducing new types as subsets of existing |
5243 types; |
5247 types; |
5244 |
5248 |
5245 :mode=text:wrap=hard:maxLineLen=72: |
5249 :mode=text:wrap=hard:maxLineLen=72: |
|
5250 |
5246 $Id$ |
5251 $Id$ |