src/Pure/basis.ML
changeset 11852 a528a716a312
parent 5836 90f7d9f1a0cc
child 13037 f7f29f8380ce
equal deleted inserted replaced
11851:d190028f43c5 11852:a528a716a312
   139   type instream = instream
   139   type instream = instream
   140   and  outstream = outstream
   140   and  outstream = outstream
   141   exception Io of {name: string, function: string, cause: exn}
   141   exception Io of {name: string, function: string, cause: exn}
   142   val stdIn 	= std_in
   142   val stdIn 	= std_in
   143   val stdOut 	= std_out
   143   val stdOut 	= std_out
       
   144   val stdErr 	= std_err
   144   val openIn 	= open_in
   145   val openIn 	= open_in
   145   val openAppend = open_append
   146   val openAppend = open_append
   146   val openOut 	= open_out
   147   val openOut 	= open_out
   147   val closeIn 	= close_in
   148   val closeIn 	= close_in
   148   val closeOut 	= close_out
   149   val closeOut 	= close_out