changeset 69468 | 54a95e1199cb |
parent 69237 | 76696742fd30 |
child 69769 | c19a32cb9625 |
--- a/src/Pure/library.ML Thu Dec 13 21:36:09 2018 +0100 +++ b/src/Pure/library.ML Fri Dec 14 11:35:21 2018 +0100 @@ -599,6 +599,7 @@ fun suffixes xs = [] :: suffixes1 xs; + (** integers **) (* lists of integers *) @@ -794,6 +795,7 @@ in match (space_explode "*" pat) str end; + (** reals **) val string_of_real = Real.fmt (StringCvt.GEN NONE);