On 2017-08-21 02:31 + wrote:
>> *Is there some solution that gives C-like automatic indentation*
>> (without having to hack SML mode)?
>
>Short answer: no.
Thanks for your honest answer.
>If I run my cursor down column 0 and hit TAB at each point, the string and
>quotation both move inwards
> *Is there some solution that gives C-like automatic indentation* (without
> having to hack SML mode)?
Short answer: no.
The situation with the emacs mode is clearly far from ideal. I have long since
trained myself to use the automatic indentation facilities when I know they
will get me rough
Hello. Thanks for your reply.
On 2017-08-20 16:31 +0200 "Chun Tian (binghe)"
wrote:
>in which the two appearances of “DIVIDES_0” are perfectly aligned, so
>that if I wrongly used different names, I can find out this mistake
>immediately. The 2nd argument (the theorem statement) of store_thm, if
>
Hi,
I think everyone has his own proof script styles, and there’s no unique way of
indentions fulfilling the favor of everyone. For me, I prefer the following
style:
val DIVIDES_0 = store_thm (
"DIVIDES_0”, ``!x. x divides 0``,
metis_tac [divides_def,MULT_CLAUSES]);
or
val DIVIDES_0 =
