changeset 81706 | 7beb0cf38292 |
parent 69275 | 9bbd5497befd |
--- a/src/HOL/Option.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/Option.thy Thu Jan 02 08:37:55 2025 +0100 @@ -373,13 +373,9 @@ | constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "==" -code_reserved SML - option NONE SOME - -code_reserved OCaml - option None Some - -code_reserved Scala - Option None Some +code_reserved + (SML) option NONE SOME + and (OCaml) option None Some + and (Scala) Option None Some end