equal
deleted
inserted
replaced
40 uses of LaTeX \cite commands and old-style @{cite "name"} document |
40 uses of LaTeX \cite commands and old-style @{cite "name"} document |
41 antiquotations. |
41 antiquotations. |
42 |
42 |
43 |
43 |
44 *** HOL *** |
44 *** HOL *** |
|
45 |
|
46 * Map.map_of and lemmas moved to List. |
45 |
47 |
46 * Theory "HOL.Euclidean_Division" renamed to "HOL.Euclidean_Rings"; |
48 * Theory "HOL.Euclidean_Division" renamed to "HOL.Euclidean_Rings"; |
47 "euclidean division" typically denotes a particular division on |
49 "euclidean division" typically denotes a particular division on |
48 integers. Minor INCOMPATIBILITY. |
50 integers. Minor INCOMPATIBILITY. |
49 |
51 |