Ramana, I think it's better to say that the one time you use the assumption you should use it with FIRST_X_ASSUM or REMOVE_THEN. You can grep through the hol-light sources to get many examples, e.g. (poisson)hol_light> grep REMOVE_THEN Multivariate/* Let's get on-line help with
# help "FIRST_X_ASSUM";; ------------------------------------------------------------------- FIRST_X_ASSUM : thm_tactic -> tactic SYNOPSIS Applies theorem-tactic to first assumption possible, extracting assumption. [...] # help "REMOVE_THEN";; ------------------------------------------------------------------- REMOVE_THEN : string -> thm_tactic -> tactic SYNOPSIS Apply a theorem tactic to named assumption, removing the assumption. [...] # help "LABEL_TAC";; gives an example using USE_THEN, which is the same as REMOVE_THEN, except that it does not remove the assumption. You could use some tactical that pulls out an assumption (POP_ASSUM, FIND_ASSUM, FIRST_ASSUM, USE_THEN, REMOVE_THEN, etc.) and give it a trivial thm_tactic like (K ALL_TAC) to essentially ignore (and hence discard) the assumption and do nothing else. I think this is partly wrong, in that POP_ASSUM, FIRST_ASSUM and USE_THEN do not delete assumptions, as Adnan wanted. -- Best, Bill ------------------------------------------------------------------------------ Android apps run on BlackBerry 10 Introducing the new BlackBerry 10.2.1 Runtime for Android apps. Now with support for Jelly Bean, Bluetooth, Mapview and more. Get your Android app in front of a whole new audience. Start now. http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
