equal
deleted
inserted
replaced
91 specific "List_Permutation". Note that most notions from that |
91 specific "List_Permutation". Note that most notions from that |
92 theory are already present in theory "Permutations". INCOMPATIBILITY. |
92 theory are already present in theory "Permutations". INCOMPATIBILITY. |
93 |
93 |
94 * Lemma "permutes_induct" has been given stronger |
94 * Lemma "permutes_induct" has been given stronger |
95 hypotheses and named premises. INCOMPATIBILITY. |
95 hypotheses and named premises. INCOMPATIBILITY. |
|
96 |
|
97 * Combinator "Fun.swap" moved into separate theory "Transposition" in |
|
98 HOL-Combinatorics. INCOMPATIBILITY. |
96 |
99 |
97 |
100 |
98 *** ML *** |
101 *** ML *** |
99 |
102 |
100 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on |
103 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on |