Re: [Hol-info] Learning HOL Light

Thanks, Konrad and Mark! I sorta understood what you posted on my own, by thinking about John & Freek's Mizar-like code. And thanks to Vince, as I now have the type annotation reduction I wanted, using retypecheck code from Freek's function parse_context_term from Mizarlight/miz2a.ml, which is

[Hol-info] [fm-announcements] RV 2013 call for papers - deadline extension

CALL FOR PAPERS RV'13 Fourth International Conference on Runtime Verification *** DEADLINE EXTENSION *** INRIA Rennes, France 24-27 September 2