equal
deleted
inserted
replaced
98 less_eq_list.induct ~> less_eq_list_induct |
98 less_eq_list.induct ~> less_eq_list_induct |
99 not_le_list_length ~> Sublist.not_sub_length |
99 not_le_list_length ~> Sublist.not_sub_length |
100 |
100 |
101 INCOMPATIBILITY. |
101 INCOMPATIBILITY. |
102 |
102 |
103 * HOL/Codatatype: New (co)datatype package with support for mixed, |
103 * HOL/BNF: New (co)datatype package based on bounded natural |
104 nested recursion and interesting non-free datatypes. |
104 functors with support for mixed, nested recursion and interesting |
|
105 non-free datatypes. |
105 |
106 |
106 * HOL/Cardinals: Theories of ordinals and cardinals |
107 * HOL/Cardinals: Theories of ordinals and cardinals |
107 (supersedes the AFP entry "Ordinals_and_Cardinals"). |
108 (supersedes the AFP entry "Ordinals_and_Cardinals"). |
108 |
109 |
109 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel |
110 * Library/Debug.thy and Library/Parallel.thy: debugging and parallel |