From ed836738a16efb7721b72f6aa58f07541fd37393 Mon Sep 17 00:00:00 2001
From: tslil clingman <>
Date: Sat, 13 Jul 2024 15:07:01 +0200
Subject: [emacs] cleanup

---
 emacs/inits/25-theorems.el | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'emacs/inits/25-theorems.el')

diff --git a/emacs/inits/25-theorems.el b/emacs/inits/25-theorems.el
index fda7ed5..51426b3 100644
--- a/emacs/inits/25-theorems.el
+++ b/emacs/inits/25-theorems.el
@@ -1,4 +1,4 @@
-;; Time-stamp: <2024-02-19 18h48 CET (anker)>
+;; Time-stamp: <2024-07-13 15h02 CEST (471b3659)>
 
 ;; -----------------------------------------------------------------------------
 ;; Coq
@@ -111,8 +111,8 @@
   )
 
 (use-package proof-general
-  :ensure t
-  :defer t
+  :ensure
+  :defer
   :functions coq-local-environment
   :init (setq proof-splash-enable nil
               proof-follow-mode 'followdown)
@@ -132,19 +132,19 @@
 ;; -----------------------------------------------------------------------------
 ;; Agda
 
-(load-file (let ((coding-system-for-read 'utf-8))
-             (shell-command-to-string "agda-mode locate")))
+;; (load-file (let ((coding-system-for-read 'utf-8))
+;;              (shell-command-to-string "agda-mode locate")))
 
-(add-hook 'agda2-mode
-          (lambda ()
-            (subword-mode 1)
-            (auto-fill-mode)
-            (aggressive-indent-mode -1)))
+;; (add-hook 'agda2-mode
+;;           (lambda ()
+;;             (subword-mode 1)
+;;             (auto-fill-mode)
+;;             (aggressive-indent-mode -1)))
 
 ;; -----------------------------------------------------------------------------
 ;; Lean
 
-(use-package lean4-mode
-  :load-path "~/.emacs.d/lean4-mode"
-  :defer t
-  :mode ("\\.lean$" . lean4-mode))
+;; (use-package lean-mode
+;;   :ensure t
+;;   :defer t
+;;   :mode ("\\.lean$" . lean-mode))
-- 
cgit v1.2.3