--- a/.emacs-my	Wed May 09 23:28:38 2012 +0300
+++ b/.emacs-my	Sat May 12 21:33:24 2012 +0300
@@ -2147,14 +2147,20 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (message "pg, Proof General")
 
-(setq proof-splash-enable nil)
+(setq proof-splash-enable t)
 ;; (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)
+
 (eval-after-load 'proof
   '(progn
-     (proof-maths-menu-toggle 1)
-     (unicode-tokens-mode 1)
-     (proof-imenu-toggle 1)
+     ;; (proof-maths-menu-toggle 1)
+     ;; (unicode-tokens-mode 1)
+     ;; (proof-imenu-toggle 1)
      ))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;