Re: [Hol-info] Learning HOL Light

2013-07-01 Thread Bill Richter
I hope folks can help me improve my code readable.ml, which in the new subversion 166 is in hol_light/RichterHilbertAxiomGeometry/ 1) Can you pretty-print error messages in HOL Light? E.g. here: with Not_found -> failwith("missing initial \"proof\" or final \"qed;\" in "^ s) It would be nice

Re: [Hol-info] Learning HOL Light

2013-07-01 Thread Vincent Aravantinos
Hi Bill, Le 2013-07-02 à 00:00, Bill Richter a écrit : > I hope folks can help me improve my code readable.ml, which in the new > subversion 166 is in > hol_light/RichterHilbertAxiomGeometry/ > > 1) Can you pretty-print error messages in HOL Light? E.g. here: > > with Not_found -> failwith