src/Pure/library.ML
changeset 3606 5d7073700fbc
parent 3553 a148c7e7152e
child 3624 36e19fce289e
     1.1 --- a/src/Pure/library.ML	Wed Aug 06 00:29:02 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Aug 06 00:29:54 1997 +0200
     1.3 @@ -873,6 +873,8 @@
     1.4                    (rm_points (space_explode "/" (tack_on cwd file)) [])
     1.5    end;
     1.6  
     1.7 +fun file_exists file = (file_info file <> "");
     1.8 +
     1.9  
    1.10  (** misc functions **)
    1.11