changeset 75295 | 38398766be6b |
parent 74356 | 2a3fe3489bae |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/ROOT.scala Tue Mar 22 16:49:18 2022 +0100 +++ b/src/Pure/ROOT.scala Tue Mar 22 18:12:58 2022 +0100 @@ -18,6 +18,7 @@ val quote = Library.quote _ val commas = Library.commas _ val commas_quote = Library.commas_quote _ + val proper_bool = Library.proper_bool _ val proper_string = Library.proper_string _ def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list) }