[Hol-info] HOL4's ARM model- Output Simplification.

Dear developers, I am a student working on formal verification of a middle-ware. In this project as a part of this verification task, I have to convert the HOL4 step theorem's output to a simplified intermediate language which can be pr

[Hol-info] [fm-announcements] Call for Papers: Runtime Verification 2013

Apologies should you receive multiple copies of this email: CALL FOR PAPERS RV'13 Fourth International Conference on Runtime Verification INRIA Rennes, France 24-27

[Hol-info] ITP 2013 - Deadline Extension

* Extended deadline * Abstract submission deadline: 29 January 2013 (anywhere on earth) Paper submission deadline: 6 February 2013 (anywhere on earth) ITP 2013: 4th International Conference on Interactive Theorem Proving 23-26 July 2013, Rennes, France

Re: [Hol-info] HOL4's ARM model- Output Simplification.

Hi Hamed, I’m assuming that your example comes from using the tool arm_random_testingLib.arm_step_updates. If you wish to manipulate these terms then you can do so using HOL4’s collection of syntax functions (e.g. see Term, boolSyntax and wordsSyntax). These libraries can be used to destruct t