Hi list, does anybody know of something providing in HOL-Light the same functionality as the Q module in HOL4?
Typically, I don't want to write "EXISTS_TAC `x:real`" if there exists only one variable called "x" in the context and its type is `:real`. So I'd like a function where it would be enough to just provide "x" and HOL Light would find out the type of x from the context. Thanks, V. -- Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent/ ------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_sfd2d_oct _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
