The type ('a,'b) istream is an abstract type of imperative streams.
These may be created with mk_istream, advanced by next,
accessed by state, and reset with reset.
COMMENTS
Purely functional streams are well-known in functional programming, and
more elegant. However, this type proved useful in implementing some
imperative ‘gensym’-like algorithms used in HOL.