The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Default parameters for emacs 19.27.1
;; activate 8bit chars
;; ...for all new buffers
(setq default-ctl-arrow "z")
;; ...and for the still active buffer
(setq ctl-arrow "z")
;; Switch to ISO display
;(standard-display-european 1)
;(require 'iso-syntax)
(setq default-frame-alist
'(
(font . "isabelle14")
(icon-type . t)
(menu-bar-lines . 1)
(width . 80)
(height . 30)
))
(transient-mark-mode 1)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; MOUSE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(global-unset-key [mouse-3])
(global-set-key [mouse-3] 'kill-region)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; some defaults
(setq-default case-fold-search nil)
(setq fill-column 64)
(setq text-mode-hook 'turn-on-auto-fill)
(setq make-backup-files nil)
(put 'eval-expression 'disabled nil)
(setq auto-mode-alist (mapcar 'purecopy
'(("\\.c$" . c-mode)
("\\.h$" . c-mode)
("\\.tex$" . TeX-mode)
("\\.itex$" . TeX-mode)
("\\.txi$" . Texinfo-mode)
("\\.el$" . emacs-lisp-mode)
("\\.a$" . c-mode))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Note: C-c <letter> sequences are reserved for users own bindings
;;
(defun Ctl-C-prefix () ; Use Ctl-C as a command prefix
Ctl-C-keymap)
(setq Ctl-C-keymap (make-keymap)) ; allocate Ctl-C keymap table
(global-set-key "\C-c" (Ctl-C-prefix)) ; define Ctl-C function
(define-key Ctl-C-keymap "g" 'goto-line)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; define an alternate keymap
;;
(defvar cursor-map-2 (make-keymap) "for ESC-[")
(fset 'Cursor-Map-2 cursor-map-2)
(define-key esc-map "[" 'Cursor-Map-2)
(define-key esc-map "[[B" 'byte-compile-file)
(define-key esc-map "[[E" 'eval-defun)
(define-key esc-map "[[F" 'eval-current-buffer)
(define-key esc-map "[[G" 'eval-region)
(define-key esc-map "[[L" 'load-file)
(define-key esc-map "[[R" 'replace-regexp)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; AUC - TeX
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(require 'tex-site)
(setq TeX-auto-global nil)
(setq TeX-auto-local nil)
(setq-default TeX-parse-self nil)
(setq-default TeX-auto-save nil)
(setq LaTeX-default-options "german,a4,12pt")
(setq TeX-auto-untabify nil)
(setq LaTeX-mode-hook '(lambda () (local-unset-key "\"")
(auto-fill-mode 1)
))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ispell
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(setq ispell-highlight-face 'modeline)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ISABELLE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(load-file "goalify.el")
(define-key Ctl-C-keymap "G" 'goalify)
(define-key Ctl-C-keymap "U" 'ungoalify)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ISABELLE to LaTeX
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-key Ctl-C-keymap "i" '(lambda () (interactive) (insert "\\I@isa")))
(define-key Ctl-C-keymap "a" '(lambda () (interactive) (insert "\\I@")))
(define-key Ctl-C-keymap "e" '(lambda () (interactive) (insert "\\E@")))
(define-key Ctl-C-keymap "t" '(lambda () (interactive) (insert "\t")))