diff -r 53fea2ccab19 -r 7beb0cf38292 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Jan 02 08:37:52 2025 +0100 +++ b/src/HOL/HOL.thy Thu Jan 02 08:37:55 2025 +0100 @@ -2074,14 +2074,10 @@ | constant False \ (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" -code_reserved SML - bool true false - -code_reserved OCaml - bool - -code_reserved Scala - Boolean +code_reserved + (SML) bool true false + and (OCaml) bool + and (Scala) Boolean code_printing constant Not \ @@ -2101,11 +2097,9 @@ and (Haskell) "!(if (_)/ then (_)/ else (_))" and (Scala) "!((_) match {/ case true => (_)/ case false => (_)/ })" -code_reserved SML - not - -code_reserved OCaml - not +code_reserved + (SML) not + and (OCaml) not code_identifier code_module Pure \