Thanks Romana... I got these tactical very useful and got my problem solved.
--
Regards
Adnan
On Friday, February 14, 2014 4:50 PM, Ramana Kumar <[email protected]>
wrote:
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
>
>
------------------------------------------------------------------------------
Managing the Performance of Cloud-Based Applications
Take advantage of what the Cloud has to offer - Avoid Common Pitfalls.
Read the Whitepaper.
http://pubads.g.doubleclick.net/gampad/clk?id=121054471&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
