Hi, When I use match_term with some types unspecified, HOL always generates a message similar to the following:
<<HOL message: inventing new type variable names: 'a, 'b>> Is there a way to depress the message so that I don't have to see a long list of messages. Specifying the types is not a good option since the matched terms have multiple types at the same sub-term position. Thanks a lot. Lu ------------------------------------------------------------------------------ Register Now for Creativity and Technology (CaT), June 3rd, NYC. CaT is a gathering of tech-side developers & brand creativity professionals. Meet the minds behind Google Creative Lab, Visual Complexity, Processing, & iPhoneDevCamp as they present alongside digital heavyweights like Barbarian Group, R/GA, & Big Spaceship. http://p.sf.net/sfu/creativitycat-com _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
