[isabelle] Automatically formatting Isabelle proof



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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.