[Hol-info] Classical Logic and Computation 2014 in Wien - First Call for Papers

-- -- First Call for Papers --

[Hol-info] Deadline extended: FLOPS 2014 call for papers

** NEWS: Submission deadline extended. - Title, abstract, and draft paper by December 13, 2013 - Full paper by December 15, 2013 (23:59 anywhere in the world) **

Re: [Hol-info] HOL Light set comprehensions

Thanks, Rob! Can you explain how HOL4 performs the quantification with GSPEC? I would think that GSPEC would have to choose a fresh variable, and I've never understood how that's to be done, because you have know that your new fresh variable hasn't already been chosen. So I would think that