*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Automatically formatting Isabelle proof*From*: li yongjian <lyj238 at gmail.com>*Date*: Tue, 7 Jan 2014 09:14:46 +0800*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>

Dear all: I want to ask a question as follows: If I have writteln a lot of proof scripts, but I did not notice to format it. Or the proofs are automatically generated by external tools. So such a proof is typed or created proof(rule impI) assume ".... Ideally, there should be automatically indenting two spaces in the 2rd line. proof(rule impI) assume ".... Is there a hot-key to format all the proof scripts by automatically indenting? best regards! li yongjian.

- Previous by Date: [isabelle] Automatically formatting Isabelle proof
- Next by Date: Re: [isabelle] Automatically formatting Isabelle proof
- Previous by Thread: Re: [isabelle] Automatically formatting Isabelle proof
- Next by Thread: Re: [isabelle] Automatically formatting Isabelle proof
- Cl-isabelle-users January 2014 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