Re: [isabelle] sml standard library



On Mon, 7 Nov 2005, Sean McLaughlin wrote:

> functions like "space_implode" which have the wrong type, changing
> 'string' for 'char'.

It is very important to note that Isabelle proper nevers uses raw
characters internally.  The smallest textual unit is a ``symbol'', which
is represented as a string and subsumes both ASCII characters and
arbitrary named symbols \<foobar>; see Pure/General/symbol.ML for further
details.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.