63 |
63 |
64 * Theory "Permutation" in HOL-Library has been renamed to the more |
64 * Theory "Permutation" in HOL-Library has been renamed to the more |
65 specific "List_Permutation". Note that most notions from that |
65 specific "List_Permutation". Note that most notions from that |
66 theory are already present in theory "Permutations". INCOMPATIBILITY. |
66 theory are already present in theory "Permutations". INCOMPATIBILITY. |
67 |
67 |
68 * Lemma "permutes_induct" has been given named premises. |
68 * Lemma "permutes_induct" has been given stronger |
69 INCOMPATIBILITY. |
69 hypotheses and named premises. INCOMPATIBILITY. |
70 |
70 |
71 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to |
71 * Theorems "antisym" and "eq_iff" in class "order" have been renamed to |
72 "order.antisym" and "order.eq_iff", to coexist locally with "antisym" |
72 "order.antisym" and "order.eq_iff", to coexist locally with "antisym" |
73 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant |
73 and "eq_iff" from locale "ordering". INCOMPATIBILITY: significant |
74 potential for change can be avoided if interpretations of type class |
74 potential for change can be avoided if interpretations of type class |
75 "order" are replaced or augmented by interpretations of locale |
75 "order" are replaced or augmented by interpretations of locale |
76 "ordering". |
76 "ordering". |
77 |
77 |
|
78 * Theorem "swap_def" now is always qualified as "Fun.swap_def". Minor |
|
79 INCOMPATIBILITY; note that for most applications less elementary lemmas |
|
80 exists. |
78 |
81 |
79 |
82 |
80 *** ML *** |
83 *** ML *** |
81 |
84 |
82 * External bash processes are always managed by Isabelle/Scala, in |
85 * External bash processes are always managed by Isabelle/Scala, in |