equal
deleted
inserted
replaced
20 |
20 |
21 * Theory "Permutation" in HOL-Library has been renamed to the more |
21 * Theory "Permutation" in HOL-Library has been renamed to the more |
22 specific "List_Permutation". Note that most notions from that |
22 specific "List_Permutation". Note that most notions from that |
23 theory are already present in theory "Permutations". INCOMPATIBILITY. |
23 theory are already present in theory "Permutations". INCOMPATIBILITY. |
24 |
24 |
25 * Lemma "permutes_induct" has been given named premised. |
25 * Lemma "permutes_induct" has been given named premises. |
26 INCOMPATIBILITY. |
26 INCOMPATIBILITY. |
27 |
27 |
28 |
28 |
29 *** ML *** |
29 *** ML *** |
30 |
30 |