--- a/.emacs-my	Wed Jun 06 23:26:29 2012 +0300
+++ b/.emacs-my	Wed Jun 06 23:28:22 2012 +0300
@@ -2148,14 +2148,17 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (message "pg, Proof General")
 
-(setq proof-splash-enable t)
+(setq proof-splash-enable nil)
 ;; (setq proof-toolbar-enable nil)
 
-(setq isar-display:show-types t)
-(setq isar-display:show-sorts t)
-(setq isar-display:show-consts t)
-(setq isar-display:show-brackets t)
-(setq isar-display:show-main-goal t)
+(setq
+ isar-display:show-types t
+ isar-display:show-sorts t
+ isar-display:show-main-goal t
+ isar-display:show-brackets t
+ ;; Too many output, so commented:
+ ;; isar-display:show-consts t
+ )
 
 (eval-after-load 'proof
   '(progn