Thanks for correcting me, Adnan and Vince, POP_ASSUM does indeed remove the
assumption:
# help "POP_ASSUM";;
-------------------------------------------------------------------
When applied to a theorem-tactic and a goal, POP_ASSUM applies
the theorem-tactic to the first element of the assumption list,
and applies the resulting tactic to the goal without the first
assumption in its assumption list:
POP_ASSUM f ({A1;...;An} ?- t) = f (... |- A1) ({A2;...;An} ?- t)
I didn't know about K, which I guess doesn't do much:
# help "K";;
-------------------------------------------------------------------
K : 'a -> 'b -> 'a
SYNOPSIS
Forms a constant function: (K x) y = x.
Adnan, I don't know why you ever have to use K. It seems that you should be
able to remove your unwanted assumption in the process of using it, with
POP_ASSUM, REMOVE_THEN or FIRST_X_ASSUM. Why don't you tell us something about
your code? And why do you need to remove the assumptions anyway? After you
finish off a subgoal, the're gone anyway, right?
--
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
