equal
deleted
inserted
replaced
86 * Document antiquotations @{class} and @{type} for printing classes |
86 * Document antiquotations @{class} and @{type} for printing classes |
87 and type constructors. |
87 and type constructors. |
88 |
88 |
89 |
89 |
90 *** HOL *** |
90 *** HOL *** |
|
91 |
|
92 * Theory Enum (for explicit enumerations of finite types) is now part of |
|
93 the HOL-Main image. INCOMPATIBILITY: All constants of the Enum theory now |
|
94 have to be referred to by its qualified name. |
|
95 constants |
|
96 enum -> Enum.enum |
|
97 nlists -> Enum.nlists |
|
98 product -> Enum.product |
91 |
99 |
92 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to |
100 * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to |
93 avoid confusion with finite sets. INCOMPATIBILITY. |
101 avoid confusion with finite sets. INCOMPATIBILITY. |
94 |
102 |
95 * Quickcheck's generator for random generation is renamed from "code" to |
103 * Quickcheck's generator for random generation is renamed from "code" to |