equal
deleted
inserted
replaced
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 |
96 |
97 * Combinator "Fun.swap" moved into separate theory "Transposition" in |
97 * Theory "Transposition" in HOL-Combinatorics provides elementary |
98 HOL-Combinatorics. INCOMPATIBILITY. |
98 swap operation "transpose". |
|
99 |
|
100 * Combinator "Fun.swap" resolved into a mere input abbreviation |
|
101 in separate theory "Transposition" in HOL-Combinatorics. |
|
102 INCOMPATIBILITY. |
99 |
103 |
100 |
104 |
101 *** ML *** |
105 *** ML *** |
102 |
106 |
103 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on |
107 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on |