changeset 35976 | ea3d4691a8c6 |
parent 34059 | f3f0e20923a7 |
child 36692 | 54b64d4ad524 |
--- a/src/Pure/library.ML Fri Mar 26 20:28:15 2010 +0100 +++ b/src/Pure/library.ML Fri Mar 26 20:30:05 2010 +0100 @@ -774,6 +774,8 @@ | NONE => match (p :: ps) (String.substring (s, 1, size s - 1))); in match (space_explode "*" pat) str end; + + (** lists as sets -- see also Pure/General/ord_list.ML **) (* canonical operations *)