src/HOL/HOL.thy
changeset 81706 7beb0cf38292
parent 81595 ed264056f5dc
child 81954 6f2bcdfa9a19
--- 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 \<rightharpoonup>
     (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 \<rightharpoonup>
@@ -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 \<rightharpoonup>