Hi all,
I would appreciate if someone could help me to find out how I can force the
Hol4 to print its output in a user defined format. For example, using the
following code snippet:
type_abbrev("u8", ``:bool[8]``);val user_plus_def = Define `(user_plus (n:u8)
(m:u8) = (n + m))`;EVAL``user_plus 2w 3w``;
the output is :
val it = |- bap_plus (2w :bool[8]) (3w :bool[8]) = (5w :bool[8]): Abbrev.thm
I was wondering if there is way to get an output like: val it = |- bap_plus
(2w :u8) (3w :u8) = (5w :u8]): Abbrev.thm
Thanks in advance.Regards,------------------------------------------------------------------------------
Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS,
MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current
with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft
MVPs and experts. ON SALE this month only -- learn more at:
http://p.sf.net/sfu/learnnow-d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
