equal
deleted
inserted
replaced
97 "fact". INCOMPATIBILITY: need to name facts explicitly in rare |
97 "fact". INCOMPATIBILITY: need to name facts explicitly in rare |
98 situations. |
98 situations. |
99 |
99 |
100 |
100 |
101 *** HOL *** |
101 *** HOL *** |
|
102 |
|
103 * Merged theories Wellfounded_Recursion, Accessible_Part and Wellfounded_Relations |
|
104 to "Wellfounded.thy" |
102 |
105 |
103 * Explicit class "eq" for executable equality. INCOMPATIBILITY. |
106 * Explicit class "eq" for executable equality. INCOMPATIBILITY. |
104 |
107 |
105 * Class finite no longer treats UNIV as class parameter. Use class enum from |
108 * Class finite no longer treats UNIV as class parameter. Use class enum from |
106 theory Library/Enum instead to achieve a similar effect. INCOMPATIBILITY. |
109 theory Library/Enum instead to achieve a similar effect. INCOMPATIBILITY. |