> HOL4's output is: > >> BETA_CONV ``(λx. ∃y. (x = a) ∧ (y = b)) y``; > <<HOL message: inventing new type variable names: 'a, 'b>> > val it = > |- (λx. ∃y. (x = a) ∧ (y = b)) y ⇔ ∃y'. (y = a) ∧ (y' = b) > : thm
Yes the HOL4 pretty printer is better than HOL Light's in various respects. So is ProofPower's (but not in this respect). But neither distinguish between overloaded variables when both/all of them are free (although in HOL4 you can hover the mouse in Emacs or use full type annotation mode). Mark. ------------------------------------------------------------------------------ Achieve unprecedented app performance and reliability What every C/C++ and Fortran developer should know. Learn how Intel has extended the reach of its next-generation tools to help boost performance applications - inlcuding clusters. http://p.sf.net/sfu/intel-dev2devmay _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
