Re: [isabelle] make_string



On 21/06/18 02:15, Jeremy Dawson wrote:
> 
> Well, obviously I don't want to create a print function for any new
> datatype when there is one there already (now that I've been told how to
> remove all the extra crap in the output from @{make_string}).
> 
> In what way is @{make_string} not suitable for production-quality output?

Before we continue this thread, can you just explain what you are trying
to do.

There is usually no need to abuse Isabelle/ML to get things done properly.


	Makarius





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