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