Hi Liu, you have realLib open. "0" can be parsed as either a real or a num. That's why you get the warning that two resolutions are possible. The "EXISTS_TAC ``0``" fails, because ``0`` is parsed as a real, while you need a num. An explicit type annotation does the trick: So use
e (EXISTS_TAC ``0:num``); Cheers Thomas ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
