initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts
;;; Options for Proof General
;;;
;;; Examples for sensible settings:
;; keep sources clean
(custom-set-variables '(indent-tabs-mode nil))
;; retain vital AltGr behaviour, e.g. on non-US Mac OS X
;(custom-set-variables '(ns-alternate-modifier 'none))
;; longer timeout for saving persistent session
;(custom-set-variables '(proof-shell-quit-timeout 60))