equal
deleted
inserted
replaced
85 * Lemma "permutes_induct" has been given stronger |
85 * Lemma "permutes_induct" has been given stronger |
86 hypotheses and named premises. INCOMPATIBILITY. |
86 hypotheses and named premises. INCOMPATIBILITY. |
87 |
87 |
88 |
88 |
89 *** ML *** |
89 *** ML *** |
|
90 |
|
91 * ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on |
|
92 the given ML expression, in contrast to functions "try" and "can" that |
|
93 modify application of a function. |
90 |
94 |
91 * External bash processes are always managed by Isabelle/Scala, in |
95 * External bash processes are always managed by Isabelle/Scala, in |
92 contrast to Isabelle2021 where this was only done for macOS on Apple |
96 contrast to Isabelle2021 where this was only done for macOS on Apple |
93 Silicon. |
97 Silicon. |
94 |
98 |