diff --git a/CHANGELOG.org b/CHANGELOG.org
deleted file mode 100644
index 1ed62fe..0000000
--- a/CHANGELOG.org
+++ /dev/null
@@ -1,35 +0,0 @@
-#+title: Lean4-Mode - Changelog
-#+language: en
-
-* Version 1.1.2
-
-- Fix occasional errors like "The connected server(s) does not support
-  method =$/lean/plainGoal=" by not wrapping invocations of
-  ~lsp-protocol~ macro into ~eval-when-compile~ but rather into
-  ~eval-and-compile~.  Thus, the methods should now work, no matter
-  whether Lean4-Mode was loaded by interpreting =.el= Elisp code or by
-  loading compiled =.elc= or =.eln= files.  ([[https://github.com/leanprover-community/lean4-mode/issues/54][Bug#54]], [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table][Zulip discussion]])
-
-* Version 1.1.1
-
-- Assign all customizable user-options to the Lean4-Mode specific
-  =lean4= group.  To customize Lean4-Mode, you now need to type =M-x
-  customize-group RET lean4 RET=.
-
-* Version 1.1.0
-
-- To =lean4= customization group, add link to local info manual and
-  use Lean4-Mode Github URL as website.
-- Introduce new dependency on Elpa package =compat=.
-- Remove dependency on Elpa package Flycheck.  It is still supported
-  but not required.
-
-* Version 1.0.1
-
-- Specify Yury G. Kudryashov as maintainer.
-- Rework README.  (Now in Org format).
-- Provide README as Texi and Info manual too.
-
-* Version 1.0
-
-- Specify "Version" in Emacs-Lisp library header.
diff --git a/Makefile b/Makefile
index 89e8f6c..a848d37 100644
--- a/Makefile
+++ b/Makefile
@@ -8,3 +8,6 @@ lean4-mode.info lean4-mode.texi: README.org
 		"--eval=(require 'ox-texinfo)" \
 		'--eval=(find-file "$<")' \
 		'--eval=(org-texinfo-export-to-info)'
+
+clean:
+	rm lean4-mode.info lean4-mode.texi
diff --git a/README.org b/README.org
index ac66c63..580d652 100644
--- a/README.org
+++ b/README.org
@@ -154,7 +154,7 @@ in VS-Code) in a separate window.
 |------------------------+--------------------------------------------------------+-----------------------------------|
 | =C-c C-k=              | Echo the keystroke needed to input the symbol at point | ~quail-show-key~                  |
 | =C-c C-d=              | Recompile and reload imports                           | ~lean4-refresh-file-dependencies~ |
-| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode                       | ~lean4-std-exe~                   |
+| =C-c C-x= or =C-c C-l= | Execute Lean in stand-alone mode                       | ~lean4-execute~                   |
 | =C-c C-p C-l=          | Builds package with lake                               | ~lean4-lake-build~                |
 | =C-c C-i=              | Toggle Info-View which shows goals and errors at point | ~lean4-toggle-info-buffer~        |
 
@@ -200,3 +200,74 @@ reasons.  In principle, it is fine to have both Lean3-Mode and
 Lean4-Mode installed at the same time.  But note that Lean3-Mode uses
 the prefix =lean-= for its symbols.  E.g. you should not use
 =lean-=-prefixed commands in a buffer with Lean4-Mode as major mode.
+
+* Changelog
+
+** Upcoming Version
+
+Documentation:
+- The changelog is now part of the readme (and thus of the Info
+  manual).
+
+User interface:
+- The tool-bar menu of Lean4-Mode does not list the
+  ~flycheck-list-errors~ anymore. Please use the “Show all errors”
+  entry in Flycheck's menu instead. (Fixes [[https://github.com/leanprover-community/lean4-mode/issues/91][#91]].)
+
+Features:
+- The variable ~lean4-delete-trailing-whitespace~ has been removed
+  together with related code. Instead of reinventing the wheel,
+  Lean4-Mode demands users to use Emacs' built-in facilities for this
+  kind of use case. For example, you might want to define a function
+  that buffer-locally adds ~delete-trailing-whitespace~ to
+  ~before-save-hook~, and add that hereby defined function to
+  ~lean4-mode-hook~.
+- The variable ~lean4-autodetect-lean3~ has been removed along with
+  the command ~lean4-select-mode~ and related code. If you still use
+  legacy version 3 of Lean for some files or projects, you could
+  directory- or file-locally associate the =.lean= file extension with
+  Lean3-Mode in ~auto-mode-alist~.
+- The command ~lean4-show-version~ has been removed. Lean4-Mode now
+  assumes Lean version 4. In order to determine the minor version, you
+  may type =M-! lean --version RET= or similar.
+- The functions ~lean4-input-export-translations~ and
+  ~lean4-input-export-translations-to-stdout~ have been removed. We
+  expect that noone has been using it. If you do use it, let us know,
+  so we can reconsider our decision in case of a substantial amount of
+  users. Otherwise, please just define these functions in your Emacs
+  initialization file yourself.
+- The command ~lean4-std-exe~ has been removed. It was just the same
+  as ~lean4-execute~ which continues to exist.
+
+** Version 1.1.2 from 2024-12-10
+
+- Fix occasional errors like "The connected server(s) does not support
+  method =$/lean/plainGoal=" by not wrapping invocations of
+  ~lsp-protocol~ macro into ~eval-when-compile~ but rather into
+  ~eval-and-compile~.  Thus, the methods should now work, no matter
+  whether Lean4-Mode was loaded by interpreting =.el= Elisp code or by
+  loading compiled =.elc= or =.eln= files.  ([[https://github.com/leanprover-community/lean4-mode/issues/54][Bug#54]], [[https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table][Zulip discussion]])
+
+** Version 1.1.1 from 2024-12-02
+
+- Assign all customizable user-options to the Lean4-Mode specific
+  =lean4= group.  To customize Lean4-Mode, you now need to type =M-x
+  customize-group RET lean4 RET=.
+
+** Version 1.1.0 from 2024-12-01
+
+- To =lean4= customization group, add link to local info manual and
+  use Lean4-Mode Github URL as website.
+- Introduce new dependency on Elpa package =compat=.
+- Remove dependency on Elpa package Flycheck.  It is still supported
+  but not required.
+
+** Version 1.0.1 from 2024-11-21
+
+- Specify Yury G. Kudryashov as maintainer.
+- Rework README.  (Now in Org format).
+- Provide README as Texi and Info manual too.
+
+** Version 1.0 from 2024-11-16
+
+- Specify "Version" in Emacs-Lisp library header.
diff --git a/lean4-input.el b/lean4-input.el
index fce884f..0051b4e 100644
--- a/lean4-input.el
+++ b/lean4-input.el
@@ -307,37 +307,6 @@ Suitable for use in the :set field of `defcustom'."
 (cl-eval-when (load eval)
   (lean4-input-setup))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Export Translations
-
-(defun lean4-input-export-translations ()
-  "Export the current translations in a javascript format.
-Print (input, output) pairs in Javascript format to the buffer
-*lean4-translations*.  The output can be copy-pasted to
-leanprover.github.io/tutorial/js/input-method.js"
-  (interactive)
-  (with-current-buffer
-      (get-buffer-create "*lean4-translations*")
-    (let ((exclude-list '("\\newline")))
-      (insert "var corrections = {")
-      (--each
-          (--filter (not (member (car it) exclude-list))
-                    (lean4-input-get-translations "Lean"))
-        (let* ((input (substring (car it) 1))
-               (outputs (cdr it)))
-          (insert (format "%s:\"" (prin1-to-string input)))
-          (cond ((vectorp outputs)
-                 (insert (elt outputs 0)))
-                (t (insert-char outputs)))
-          (insert (format "\",\n"))))
-      (insert "};"))))
-
-(defun lean4-input-export-translations-to-stdout ()
-  "Print current translations to stdout."
-  (lean4-input-export-translations)
-  (with-current-buffer "*lean4-translations*"
-    (princ (buffer-string))))
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Administrative details
 
diff --git a/lean4-mode.el b/lean4-mode.el
index 3994c99..6992002 100644
--- a/lean4-mode.el
+++ b/lean4-mode.el
@@ -63,7 +63,6 @@
 (defvar markdown-code-lang-modes)
 (declare-function flycheck-list-errors "ext:flycheck")
 (declare-function flymake-proc-init-create-temp-buffer-copy "flymake-proc")
-(declare-function lean-mode "ext:lean-mode")
 (declare-function quail-show-key "quail")
 
 (defun lean4-compile-string (lake-name exe-name args file-name)
@@ -102,11 +101,6 @@ FILE-NAME."
     (setq compile-command cc)
     (setq default-directory dd)))
 
-(defun lean4-std-exe ()
-  "Execute Lean in the current buffer."
-  (interactive)
-  (lean4-execute))
-
 (defun lean4-refresh-file-dependencies ()
   "Refresh the file dependencies.
 
@@ -132,9 +126,9 @@ file, recompiling, and reloading all imports."
         (t (indent-for-tab-command))))
 
 (defun lean4-set-keys ()
-  "Setup Lean 4 keybindings."
-  (local-set-key lean4-keybinding-std-exe1                  #'lean4-std-exe)
-  (local-set-key lean4-keybinding-std-exe2                  #'lean4-std-exe)
+  "Setup Lean4 keybindings."
+  (local-set-key lean4-keybinding-std-exe1                  #'lean4-execute)
+  (local-set-key lean4-keybinding-std-exe2                  #'lean4-execute)
   (local-set-key lean4-keybinding-show-key                  #'quail-show-key)
   (local-set-key lean4-keybinding-tab-indent                #'lean4-tab-indent)
   ;; (local-set-key lean4-keybinding-hole                      #'lean4-hole)
@@ -147,9 +141,6 @@ file, recompiling, and reloading all imports."
   ;; (local-set-key (kbd "<mouse-3>")                         #'lean4-right-click-show-menu)
   )
 
-(define-abbrev-table 'lean4-abbrev-table
-  '())
-
 (defvar lean4-mode-map (make-sparse-keymap)
   "Keymap used in Lean mode.")
 
@@ -158,19 +149,11 @@ file, recompiling, and reloading all imports."
   `("Lean 4"
     ["Execute lean"         lean4-execute           t]
     ["Toggle info display"  lean4-toggle-info       t]
-    ;; TODO: Bug#91: We offers a Flycheck-based menu-item when
-    ;; Flycheck is in use.  Users who use built-in Flymake should also
-    ;; be offered a working menu-item.  Alternatively, the menu-item
-    ;; could also be dropped for both cases.
-    ["List of errors"       flycheck-list-errors    flycheck-mode]
     ["Restart lean process" lsp-workspace-restart   t]
     ["Customize lean4-mode" (customize-group 'lean) t]))
 
 (defconst lean4-hooks-alist
-  '(
-    ;; Handle events that may start automatic syntax checks
-    (before-save-hook . lean4-whitespace-cleanup)
-    ;; info view
+  '(;; info view
     ;; update errors immediately, but delay querying goal
     (flycheck-after-syntax-check-hook . lean4-info-buffer-redisplay-debounced)
     (post-command-hook . lean4-info-buffer-redisplay-debounced)
@@ -216,7 +199,6 @@ of the parent project."
 
 \\{lean4-mode-map}"
   :syntax-table lean4-syntax-table
-  :abbrev-table lean4-abbrev-table
   :group 'lean4
   (set (make-local-variable 'comment-start) "--")
   (set (make-local-variable 'comment-start-skip) "[-/]-[ \t]*")
@@ -234,41 +216,19 @@ of the parent project."
   (lean4-set-keys)
   (if (fboundp 'electric-indent-local-mode)
       (electric-indent-local-mode -1))
-  ;; (abbrev-mode 1)
   (pcase-dolist (`(,hook . ,fn) lean4-hooks-alist)
     (add-hook hook fn nil 'local))
   (lean4-mode-setup))
 
-(defun lean4--version ()
-  "Return Lean version as a list `(MAJOR MINOR PATCH)'."
-  (with-temp-buffer
-    (call-process (lean4-get-executable "lean") nil (list t nil) nil "-v")
-    (goto-char (point-min))
-    (re-search-forward (rx bol "Lean (version " (group (+ digit) (+ "." (+ digit)))))
-    (version-to-list (match-string 1))))
-
-(defun lean4-show-version ()
-  "Print Lean 4 version."
-  (interactive)
-  (message "Lean %s" (mapconcat #'number-to-string (lean4--version) ".")))
-
-;;;###autoload
-(defun lean4-select-mode ()
-  "Automatically select mode (Lean 3 vs Lean 4)."
-  (if (and lean4-autodetect-lean3
-           (eq 3 (car (lean4--version))))
-      (lean-mode)
-    (lean4-mode)))
-
 ;; Automatically use lean4-mode for .lean files.
 ;;;###autoload
 (add-to-list 'auto-mode-alist
-             '("\\.lean\\'" . lean4-select-mode))
+             '("\\.lean\\'" . lean4-mode))
 
 ;;;###autoload
 (with-eval-after-load 'markdown-mode
   (add-to-list 'markdown-code-lang-modes
-               '("lean" . lean4-select-mode)))
+               '("lean" . lean4-mode)))
 
 ;; Use utf-8 encoding
 ;;;### autoload
diff --git a/lean4-mode.info b/lean4-mode.info
index 41a8f4c..6c1cf8a 100644
--- a/lean4-mode.info
+++ b/lean4-mode.info
@@ -32,6 +32,7 @@ Lean's Zulip chat.
 * Usage::
 * Configuration::
 * Common Pitfalls::
+* Changelog::
 
 -- The Detailed Node Listing --
 
@@ -57,6 +58,15 @@ Configuration
 * lsp-mode: lsp-mode (1).
 * Flycheck: Flycheck (1).
 
+Changelog
+
+* Upcoming Version::
+* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10.
+* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02.
+* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01.
+* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21.
+* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16.
+
 
 
 File: lean4-mode.info,  Node: Installation,  Next: Usage,  Prev: Top,  Up: Top
@@ -230,7 +240,7 @@ Key                      Description
 ----------------------------------------------------------------------------------------------------------------------
 ‘C-c C-k’                Echo the keystroke needed to input the symbol at point   ‘quail-show-key’
 ‘C-c C-d’                Recompile and reload imports                             ‘lean4-refresh-file-dependencies’
-‘C-c C-x’ or ‘C-c C-l’   Execute Lean in stand-alone mode                         ‘lean4-std-exe’
+‘C-c C-x’ or ‘C-c C-l’   Execute Lean in stand-alone mode                         ‘lean4-execute’
 ‘C-c C-p C-l’            Builds package with lake                                 ‘lean4-lake-build’
 ‘C-c C-i’                Toggle Info-View which shows goals and errors at point   ‘lean4-toggle-info-buffer’
 
@@ -300,7 +310,7 @@ installed, then customize the ‘lsp-diagnostics-provider’ user option
 accordingly.
 
 
-File: lean4-mode.info,  Node: Common Pitfalls,  Prev: Configuration,  Up: Top
+File: lean4-mode.info,  Node: Common Pitfalls,  Next: Changelog,  Prev: Configuration,  Up: Top
 
 4 Common Pitfalls
 *****************
@@ -313,24 +323,143 @@ note that Lean3-Mode uses the prefix ‘lean-’ for its symbols.  E.g.  you
 should not use ‘lean-’-prefixed commands in a buffer with Lean4-Mode as
 major mode.
 
+
+File: lean4-mode.info,  Node: Changelog,  Prev: Common Pitfalls,  Up: Top
+
+5 Changelog
+***********
+
+* Menu:
+
+* Upcoming Version::
+* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10.
+* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02.
+* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01.
+* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21.
+* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16.
+
+
+File: lean4-mode.info,  Node: Upcoming Version,  Next: Version 112 from 2024-12-10,  Up: Changelog
+
+5.1 Upcoming Version
+====================
+
+Documentation:
+   • The changelog is now part of the readme (and thus of the Info
+     manual).
+
+   User interface:
+   • The tool-bar menu of Lean4-Mode does not list the
+     ‘flycheck-list-errors’ anymore.  Please use the “Show all errors”
+     entry in Flycheck's menu instead.  (Fixes #91
+     (https://github.com/leanprover-community/lean4-mode/issues/91).)
+
+   Features:
+   • The variable ‘lean4-delete-trailing-whitespace’ has been removed
+     together with related code.  Instead of reinventing the wheel,
+     Lean4-Mode demands users to use Emacs' built-in facilities for this
+     kind of use case.  For example, you might want to define a function
+     that buffer-locally adds ‘delete-trailing-whitespace’ to
+     ‘before-save-hook’, and add that hereby defined function to
+     ‘lean4-mode-hook’.
+   • The variable ‘lean4-autodetect-lean3’ has been removed along with
+     the command ‘lean4-select-mode’ and related code.  If you still use
+     legacy version 3 of Lean for some files or projects, you could
+     directory- or file-locally associate the ‘.lean’ file extension
+     with Lean3-Mode in ‘auto-mode-alist’.
+   • The command ‘lean4-show-version’ has been removed.  Lean4-Mode now
+     assumes Lean version 4.  In order to determine the minor version,
+     you may type ‘M-! lean --version RET’ or similar.
+   • The functions ‘lean4-input-export-translations’ and
+     ‘lean4-input-export-translations-to-stdout’ have been removed.  We
+     expect that noone has been using it.  If you do use it, let us
+     know, so we can reconsider our decision in case of a substantial
+     amount of users.  Otherwise, please just define these functions in
+     your Emacs initialization file yourself.
+   • The command ‘lean4-std-exe’ has been removed.  It was just the same
+     as ‘lean4-execute’ which continues to exist.
+
+
+File: lean4-mode.info,  Node: Version 112 from 2024-12-10,  Next: Version 111 from 2024-12-02,  Prev: Upcoming Version,  Up: Changelog
+
+5.2 Version 1.1.2 from 2024-12-10
+=================================
+
+   • Fix occasional errors like "The connected server(s) does not
+     support method ‘$/lean/plainGoal’" by not wrapping invocations of
+     ‘lsp-protocol’ macro into ‘eval-when-compile’ but rather into
+     ‘eval-and-compile’.  Thus, the methods should now work, no matter
+     whether Lean4-Mode was loaded by interpreting ‘.el’ Elisp code or
+     by loading compiled ‘.elc’ or ‘.eln’ files.  (Bug#54
+     (https://github.com/leanprover-community/lean4-mode/issues/54),
+     Zulip discussion
+     (https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table))
+
+
+File: lean4-mode.info,  Node: Version 111 from 2024-12-02,  Next: Version 110 from 2024-12-01,  Prev: Version 112 from 2024-12-10,  Up: Changelog
+
+5.3 Version 1.1.1 from 2024-12-02
+=================================
+
+   • Assign all customizable user-options to the Lean4-Mode specific
+     ‘lean4’ group.  To customize Lean4-Mode, you now need to type ‘M-x
+     customize-group RET lean4 RET’.
+
+
+File: lean4-mode.info,  Node: Version 110 from 2024-12-01,  Next: Version 101 from 2024-11-21,  Prev: Version 111 from 2024-12-02,  Up: Changelog
+
+5.4 Version 1.1.0 from 2024-12-01
+=================================
+
+   • To ‘lean4’ customization group, add link to local info manual and
+     use Lean4-Mode Github URL as website.
+   • Introduce new dependency on Elpa package ‘compat’.
+   • Remove dependency on Elpa package Flycheck.  It is still supported
+     but not required.
+
+
+File: lean4-mode.info,  Node: Version 101 from 2024-11-21,  Next: Version 10 from 2024-11-16,  Prev: Version 110 from 2024-12-01,  Up: Changelog
+
+5.5 Version 1.0.1 from 2024-11-21
+=================================
+
+   • Specify Yury G.  Kudryashov as maintainer.
+   • Rework README.  (Now in Org format).
+   • Provide README as Texi and Info manual too.
+
+
+File: lean4-mode.info,  Node: Version 10 from 2024-11-16,  Prev: Version 101 from 2024-11-21,  Up: Changelog
+
+5.6 Version 1.0 from 2024-11-16
+===============================
+
+   • Specify "Version" in Emacs-Lisp library header.
+
 
 
 Tag Table:
 Node: Top223
-Node: Installation1492
-Node: Brief and Generic Instructions1735
-Node: Detailed and Concrete Instructions2684
-Node: Instructions for Source-Based Use-Package4341
-Node: Native vc (Emacs 30 or later)5062
-Node: Doom-Emacs5970
-Node: Straight6396
-Node: Usage6896
-Node: lsp-mode8342
-Node: Flycheck8627
-Node: Configuration9237
-Node: lsp-mode (1)9427
-Node: Flycheck (1)9696
-Node: Common Pitfalls10181
+Node: Installation1846
+Node: Brief and Generic Instructions2089
+Node: Detailed and Concrete Instructions3038
+Node: Instructions for Source-Based Use-Package4695
+Node: Native vc (Emacs 30 or later)5416
+Node: Doom-Emacs6324
+Node: Straight6750
+Node: Usage7250
+Node: lsp-mode8696
+Node: Flycheck8981
+Node: Configuration9591
+Node: lsp-mode (1)9781
+Node: Flycheck (1)10050
+Node: Common Pitfalls10535
+Node: Changelog11127
+Node: Upcoming Version11567
+Node: Version 112 from 2024-12-1013633
+Node: Version 111 from 2024-12-0214498
+Node: Version 110 from 2024-12-0114905
+Node: Version 101 from 2024-11-2115403
+Node: Version 10 from 2024-11-1615766
 
 End Tag Table
 
diff --git a/lean4-mode.texi b/lean4-mode.texi
index fd205bf..cfc6cee 100644
--- a/lean4-mode.texi
+++ b/lean4-mode.texi
@@ -40,6 +40,7 @@ as @emph{Lean-Mode}).
 * Usage::
 * Configuration::
 * Common Pitfalls::
+* Changelog::
 
 @detailmenu
 --- The Detailed Node Listing ---
@@ -66,6 +67,15 @@ Configuration
 * lsp-mode: lsp-mode (1). 
 * Flycheck: Flycheck (1). 
 
+Changelog
+
+* Upcoming Version::
+* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. 
+* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. 
+* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. 
+* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. 
+* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. 
+
 @end detailmenu
 @end menu
 
@@ -242,7 +252,7 @@ in VS-Code) in a separate window.
 @tab @code{lean4-refresh-file-dependencies}
 @item @samp{C-c C-x} or @samp{C-c C-l}
 @tab Execute Lean in stand-alone mode
-@tab @code{lean4-std-exe}
+@tab @code{lean4-execute}
 @item @samp{C-c C-p C-l}
 @tab Builds package with lake
 @tab @code{lean4-lake-build}
@@ -317,4 +327,123 @@ Lean4-Mode installed at the same time.  But note that Lean3-Mode uses
 the prefix @samp{lean-} for its symbols.  E.g. you should not use
 @samp{lean-}-prefixed commands in a buffer with Lean4-Mode as major mode.
 
+@node Changelog
+@chapter Changelog
+
+@menu
+* Upcoming Version::
+* Version 1.1.2 from 2024-12-10: Version 112 from 2024-12-10. 
+* Version 1.1.1 from 2024-12-02: Version 111 from 2024-12-02. 
+* Version 1.1.0 from 2024-12-01: Version 110 from 2024-12-01. 
+* Version 1.0.1 from 2024-11-21: Version 101 from 2024-11-21. 
+* Version 1.0 from 2024-11-16: Version 10 from 2024-11-16. 
+@end menu
+
+@node Upcoming Version
+@section Upcoming Version
+
+Documentation:
+@itemize
+@item
+The changelog is now part of the readme (and thus of the Info
+manual).
+@end itemize
+
+User interface:
+@itemize
+@item
+The tool-bar menu of Lean4-Mode does not list the
+@code{flycheck-list-errors} anymore. Please use the “Show all errors”
+entry in Flycheck's menu instead. (Fixes @uref{https://github.com/leanprover-community/lean4-mode/issues/91, #91}.)
+@end itemize
+
+Features:
+@itemize
+@item
+The variable @code{lean4-delete-trailing-whitespace} has been removed
+together with related code. Instead of reinventing the wheel,
+Lean4-Mode demands users to use Emacs' built-in facilities for this
+kind of use case. For example, you might want to define a function
+that buffer-locally adds @code{delete-trailing-whitespace} to
+@code{before-save-hook}, and add that hereby defined function to
+@code{lean4-mode-hook}.
+@item
+The variable @code{lean4-autodetect-lean3} has been removed along with
+the command @code{lean4-select-mode} and related code. If you still use
+legacy version 3 of Lean for some files or projects, you could
+directory- or file-locally associate the @samp{.lean} file extension with
+Lean3-Mode in @code{auto-mode-alist}.
+@item
+The command @code{lean4-show-version} has been removed. Lean4-Mode now
+assumes Lean version 4. In order to determine the minor version, you
+may type @samp{M-! lean --version RET} or similar.
+@item
+The functions @code{lean4-input-export-translations} and
+@code{lean4-input-export-translations-to-stdout} have been removed. We
+expect that noone has been using it. If you do use it, let us know,
+so we can reconsider our decision in case of a substantial amount of
+users. Otherwise, please just define these functions in your Emacs
+initialization file yourself.
+@item
+The command @code{lean4-std-exe} has been removed. It was just the same
+as @code{lean4-execute} which continues to exist.
+@end itemize
+
+@node Version 112 from 2024-12-10
+@section Version 1.1.2 from 2024-12-10
+
+@itemize
+@item
+Fix occasional errors like "The connected server(s) does not support
+method @samp{$/lean/plainGoal}" by not wrapping invocations of
+@code{lsp-protocol} macro into @code{eval-when-compile} but rather into
+@code{eval-and-compile}.  Thus, the methods should now work, no matter
+whether Lean4-Mode was loaded by interpreting @samp{.el} Elisp code or by
+loading compiled @samp{.elc} or @samp{.eln} files.  (@uref{https://github.com/leanprover-community/lean4-mode/issues/54, Bug#54}, @uref{https://leanprover.zulipchat.com/#narrow/channel/468104-Emacs/topic/lsp-mode.20errors.20due.20to.20list.20!.3D.20hash-table, Zulip discussion})
+@end itemize
+
+@node Version 111 from 2024-12-02
+@section Version 1.1.1 from 2024-12-02
+
+@itemize
+@item
+Assign all customizable user-options to the Lean4-Mode specific
+@samp{lean4} group.  To customize Lean4-Mode, you now need to type @samp{M-x
+  customize-group RET lean4 RET}.
+@end itemize
+
+@node Version 110 from 2024-12-01
+@section Version 1.1.0 from 2024-12-01
+
+@itemize
+@item
+To @samp{lean4} customization group, add link to local info manual and
+use Lean4-Mode Github URL as website.
+@item
+Introduce new dependency on Elpa package @samp{compat}.
+@item
+Remove dependency on Elpa package Flycheck.  It is still supported
+but not required.
+@end itemize
+
+@node Version 101 from 2024-11-21
+@section Version 1.0.1 from 2024-11-21
+
+@itemize
+@item
+Specify Yury G@. Kudryashov as maintainer.
+@item
+Rework README@.  (Now in Org format).
+@item
+Provide README as Texi and Info manual too.
+@end itemize
+
+@node Version 10 from 2024-11-16
+@section Version 1.0 from 2024-11-16
+
+@itemize
+@item
+Specify "Version" in Emacs-Lisp library header.
+@end itemize
+
 @bye
diff --git a/lean4-settings.el b/lean4-settings.el
index 910e533..24a4f2c 100644
--- a/lean4-settings.el
+++ b/lean4-settings.el
@@ -90,14 +90,6 @@ It is approximately the maximum number of memory allocations in thousands."
   :group 'lean4
   :type '(list string))
 
-(defcustom lean4-delete-trailing-whitespace nil
-  "Automatically delete trailing shitespace.
-Set this variable to true to automatically delete trailing
-whitespace when a buffer is loaded from a file or when it is
-written."
-  :group 'lean4
-  :type 'boolean)
-
 (defcustom lean4-highlight-inaccessible-names t
   "Use font to highlight inaccessible names.
 Set this variable to t to highlight inaccessible names in the info display
@@ -110,20 +102,11 @@ using `font-lock-comment-face' instead of the `✝` suffix used by Lean."
   :group 'lean4
   :type 'boolean)
 
-
-(defcustom lean4-autodetect-lean3 nil
-  "Autodetect Lean version.
-Use elan to check if current project uses Lean 3 or Lean 4 and initialize the
-right mode when visiting a file.  If elan has a default Lean version, Lean files
-outside a project will default to that mode."
-  :group 'lean4
-  :type 'boolean)
-
 (defcustom lean4-keybinding-std-exe1 (kbd "C-c C-x")
-  "Main Keybinding for `lean4-std-exe'."
+  "Main Keybinding for `lean4-execute'."
   :group 'lean4-keybinding :type 'key-sequence)
 (defcustom lean4-keybinding-std-exe2 (kbd "C-c C-l")
-  "Alternative Keybinding for `lean4-std-exe'."
+  "Alternative Keybinding for `lean4-execute'."
   :group 'lean4-keybinding  :type 'key-sequence)
 (defcustom lean4-keybinding-show-key (kbd "C-c C-k")
   "Lean Keybinding for `quail-show-key'."
diff --git a/lean4-util.el b/lean4-util.el
index 273a530..2b8cdab 100644
--- a/lean4-util.el
+++ b/lean4-util.el
@@ -55,10 +55,5 @@ First try to find an executable named `lean4-executable-name' in
   "Return fullpath of lean executable EXE-NAME."
   (file-name-concat (lean4-get-rootdir) "bin" exe-name))
 
-(defun lean4-whitespace-cleanup ()
-  "Delete trailing whitespace if `lean4-delete-trailing-whitespace' is t."
-  (when lean4-delete-trailing-whitespace
-      (delete-trailing-whitespace)))
-
 (provide 'lean4-util)
 ;;; lean4-util.el ends here