--- a/src/HOL/HOL.thy Fri Apr 05 20:41:54 2024 +0200
+++ b/src/HOL/HOL.thy Fri Apr 05 21:21:02 2024 +0200
@@ -2067,12 +2067,12 @@
(SML) "!(if (_)/ then (_)/ else true)"
and (OCaml) "!(if (_)/ then (_)/ else true)"
and (Haskell) "!(if (_)/ then (_)/ else True)"
- and (Scala) "!(if ((_))/ (_)/ else true)"
+ and (Scala) "!((_) match {/ case true => (_)/ case false => true/ })"
| constant If \<rightharpoonup>
(SML) "!(if (_)/ then (_)/ else (_))"
and (OCaml) "!(if (_)/ then (_)/ else (_))"
and (Haskell) "!(if (_)/ then (_)/ else (_))"
- and (Scala) "!(if ((_))/ (_)/ else (_))"
+ and (Scala) "!((_) match {/ case true => (_)/ case false => (_)/ })"
code_reserved SML
not