src/Pure/basis.ML
changeset 13037 f7f29f8380ce
parent 11852 a528a716a312
equal deleted inserted replaced
13036:dca23533bdfb 13037:f7f29f8380ce
   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 stdErr 	= std_out
   145   val openIn 	= open_in
   145   val openIn 	= open_in
   146   val openAppend = open_append
   146   val openAppend = open_append
   147   val openOut 	= open_out
   147   val openOut 	= open_out
   148   val closeIn 	= close_in
   148   val closeIn 	= close_in
   149   val closeOut 	= close_out
   149   val closeOut 	= close_out