On 2012-08-01 12:09, Serge D. Mechveliani wrote: > 2. As \bn works now, and emacs displayes math symbols as needed, > do I need further to issue the commands to > _customize_ emacs to Agda, to set an _input method_ ? No. The Agda input method is turned on when the Agda mode is initialised. -- /NAD