Lars just informed me that I didn't actually include an example in my
mail (I thought I did); it was therefore probably not clear what I meant
exactly, so let me explain:
When I write "\ci" in a theory, it used to be completed to ∘
immediately. As of 1ca11ddfcc70, this does not happen anymore; I have to
complete it manually. The same happens with every other backslash
abbreviation I tried. Is this the intended behaviour? If it is, I'm
afraid I find that somewhat unpleasant.
As an unrelated issue: convergence of functions/sequences is written as
"op --->" / "op ---->". Entering this arrow is somewhat painful when
immediate completion is turned on, since it completes to "-⟶" / "--⟶".
Is there anything that can be done about that?
Cheers,
Manuel
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
