changeset 81706 | 7beb0cf38292 |
parent 72671 | 588c751a5eef |
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Thu Jan 02 08:37:55 2025 +0100 @@ -655,7 +655,7 @@ return a }" -code_reserved SML upto +code_reserved (SML) upto definition "example = do { a \<leftarrow> Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list);