tuned white space;
authorwenzelm
Fri Mar 26 20:30:05 2010 +0100 (2010-03-26)
changeset 35976ea3d4691a8c6
parent 35975 cef3c78ace0a
child 35978 6343ebe9715d
tuned white space;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Mar 26 20:28:15 2010 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Mar 26 20:30:05 2010 +0100
     1.3 @@ -774,6 +774,8 @@
     1.4              | NONE => match (p :: ps) (String.substring (s, 1, size s - 1)));
     1.5    in match (space_explode "*" pat) str end;
     1.6  
     1.7 +
     1.8 +
     1.9  (** lists as sets -- see also Pure/General/ord_list.ML **)
    1.10  
    1.11  (* canonical operations *)