# HG changeset patch # User wenzelm # Date 1269631805 -3600 # Node ID ea3d4691a8c6e50192ac88236d68147c04bcd676 # Parent cef3c78ace0adeae6522c51414c11232e535e12d tuned white space; diff -r cef3c78ace0a -r ea3d4691a8c6 src/Pure/library.ML --- 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 *)