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.
On Thu, Feb 13, 2014 at 4:03 AM, Adnan Rashid Raja
<[email protected]>wrote:
> Dear all,
>
> I am working in HOL-Light. Can I find any tactics which can be used to
> delete the assumptions which are generated during the proof. These
> assumptions are used once, and of no need in future.
>
> --
> Regards
> Adnan
>
>
> ------------------------------------------------------------------------------
> 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
>
>
------------------------------------------------------------------------------
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
