equal
deleted
inserted
replaced
37 "fact". INCOMPATIBILITY: need to name facts explicitly in rare |
37 "fact". INCOMPATIBILITY: need to name facts explicitly in rare |
38 situations. |
38 situations. |
39 |
39 |
40 |
40 |
41 *** HOL *** |
41 *** HOL *** |
|
42 |
|
43 * Theory Nat: renamed less_imp_le to less_imp_le_nat; removed |
|
44 redundant lemmas less_trans, less_linear, le_imp_less_or_eq, |
|
45 le_less_trans, less_le_trans, which merely duplicate lemmas of the |
|
46 same name in theory Orderings. Potential INCOMPATIBILITY due to more |
|
47 general and different variable names. |
42 |
48 |
43 * Library/Option_ord.thy: Canonical order on option type. |
49 * Library/Option_ord.thy: Canonical order on option type. |
44 |
50 |
45 * Library/RBT.thy: New theory of red-black trees, an efficient |
51 * Library/RBT.thy: New theory of red-black trees, an efficient |
46 implementation of finite maps. |
52 implementation of finite maps. |