changeset 81706 | 7beb0cf38292 |
parent 81595 | ed264056f5dc |
child 81744 | 9714d5b221e2 |
--- a/src/HOL/List.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/List.thy Thu Jan 02 08:37:55 2025 +0100 @@ -8089,11 +8089,9 @@ setup \<open>fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]\<close> -code_reserved SML - list - -code_reserved OCaml - list +code_reserved + (SML) list + and (OCaml) list subsubsection \<open>Use convenient predefined operations\<close>