Email Gateway (Aug 19 2022 at 13:19): Email Gateway (Aug 19 2022 at 13:19):From: li yongjian <lyj238@gmail.com>
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.
Email Gateway (Aug 19 2022 at 13:20):From: li yongjian <lyj238@gmail.com>
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.
Email Gateway (Aug 19 2022 at 13:21):From: li yongjian <lyj238@gmail.com>
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.
Email Gateway (Aug 19 2022 at 13:22):From: li yongjian <lyj238@gmail.com>
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.
Email Gateway (Aug 19 2022 at 13:23):From: Lars Noschinski <noschinl@in.tum.de>
Isabelle/jEdit has no option to do code formatting, however the old
ProofGeneral interface can do this.
Email Gateway (Aug 19 2022 at 13:24):From: li yongjian <lyj238@gmail.com>
I>sabelle/jEdit has no option to do code formatting, however the old
ProofGeneral interface can do this.
How to do this in old
ProofGeneral interface, I can use emacs interface to do it.
Email Gateway (Aug 19 2022 at 13:25):From: li yongjian <lyj238@gmail.com>
I>sabelle/jEdit has no option to do code formatting, however the old
ProofGeneral interface can do this.
How to do this in old
ProofGeneral interface, I can use emacs interface to do it.
Email Gateway (Aug 19 2022 at 13:26):From: "Jens-D. Doll" <jd@cococo.de>
Elbe contains this facility regardless of language. I am currently
considering an update of the software. If somebody was willing to help me
we could build an Isabelle formatter very soon
[http://cococo.de/Elbe]
Greetings and wishes for a good 2014
Jens
Email Gateway (Aug 19 2022 at 13:27):From: li yongjian <lyj238@gmail.com>
I have downloaded Elbe, but it seems that this is not a free software?
I cannot use it.
Email Gateway (Aug 19 2022 at 13:27):From: "Jens-D. Doll" <jd@cococo.de>
Hello Li,
this is not quite correct. If you have a student email address, containing
e.g. ".edu" or "university", you can request a free academic license.
Use the menu item of Elbe, see attachment, which leads you to the
licensing web page.
Are you willing to help me?
Jens
academic.jpg
Email Gateway (Aug 19 2022 at 13:32):From: lyj238 <lyj238@gmail.com>
Elbe contains this facility regardless of language. I am currently
considering an update of the software. If somebody was willing to help me
we could build an Isabelle formatter very soon
[http://cococo.de/Elbe]
Greetings and wishes for a good 2014
Jens
Email Gateway (Aug 19 2022 at 15:02):From: yongjian Li <lyj238@ios.ac.cn>
I have an email adr with suffix ac.cn.
I can help you.
Email Gateway (Aug 19 2022 at 15:05):From: "Jens-D. Doll" <jd@cococo.de>
Hello Li and all,
thanks for the offering. Could you click on menu item Help.Get Academic
License, which should produce an URL like
and fill out the form?
What does the server answer? Pls. send a screen shot and tell me the IP
address of your client.
Greetings,
Jens
Last updated: Apr 25 2024 at 20:15 UTC