*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] The development of a large proof script.*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Wed, 04 Feb 2015 14:33:03 +0100*In-reply-to*: <201502042111505364572@ios.ac.cn>*References*: <201502042111505364572@ios.ac.cn>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Dear lyj238, maybe you could give as some more details?

cheers chris On 02/04/2015 02:18 PM, lyj238 at ios.ac.cn wrote:

Dear experts: Now I want to ask some details on the development of a large proof script. A proof script on a real protocol case study has 20 MB. It is really beyond the ability of Isabelle's JEDIT interface. I have used the tty model to run a smaller script with 2MBs in batch in previous Isabelle 2012. But it is very inconvenient, and the tty model is not supported by Isabelle 2014. (1) How to run the larger proof in Isabelle 2014? (2)Essentially, my proof script contain a main lemma and thousands of basic lemmas which is used in the proof of the main lemma. The proof of thousands of basic lemmas can be proved in parallel. Parallel proof (or distributing proofs) are supported by Isabelle 2014? Best regards! lyj238 at ios.ac.cn

**References**:**[isabelle] The development of a large proof script.***From:*lyj238 at ios.ac.cn

- Previous by Date: Re: [isabelle] The development of a large proof script.
- Next by Date: [isabelle] Changes in the use of the tab key
- Previous by Thread: Re: [isabelle] The development of a large proof script.
- Next by Thread: Re: [isabelle] 回复: Re: The development of a large proof script.
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list