diff --git a/tla+-mode.el b/tla+-mode.el
index 49fb78c..c8aab99 100644
--- a/tla+-mode.el
+++ b/tla+-mode.el
@@ -38,7 +38,11 @@
 ;;        (load "/path/to/tla+-mode.el")
 ;;    and use it with
 ;;        (require tla+-mode)
-
+;;
+;; Getting, and Using the tlatoolbox:
+;;   https://tla.msr-inria.inria.fr/tlatoolbox/dist/
+;;   https://lamport.azurewebsites.net/tla/tools.html
+;;   https://lamport.azurewebsites.net/tla/standalone-tools.html
 
 ;;; Code:
 
@@ -449,7 +453,8 @@ Operation:
       (switch-to-buffer sanybuffer)
       (erase-buffer)
       (insert output)
-      (tla+/find-error-marks))))
+      (tla+/find-error-marks)
+      (other-window 1))))
 
 (defun tla+-run-model (cfgfile)
   "Run the tlc2.TLC Model checker
@@ -487,6 +492,7 @@ Note: The TLA+ specification file is a relative path.
       (switch-to-buffer tlcbuffer)
       (erase-buffer)
       (insert output)
+      (other-window 1)
       (message  (concat "cmd: " cmd))
       )))