Fair enough, I guess I just need to include the file that does temp_add_user_printer. I think the problem I was thinking of is that add_user_printer is basically useless (I feel like I've brought that up before, but couldn't find it).
Thanks for the prod to just use a userprinter! On Thu, Oct 23, 2014 at 10:54 PM, Michael Norrish < michael.norr...@nicta.com.au> wrote: > > > > On 24 Oct 2014, at 04:59, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> > wrote: > > > (Userprinters are very difficult to use with the munger, so I would > like to avoid them if possible.) > > Why is this? Note that printing of if-then-else and monad syntax is done > by a user printer in core HOL, and those examples work fine in the munger. > > Michael > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
