From 628a05ec0bc271e8b0d70b009d6a31a37e9f9c68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ren=C3=A9=20Neumann?= <rene.neumann@in.tum.de>
Date: Tue, 6 Mar 2012 16:54:49 +0100
Subject: More isabelle emacs stuff, especially shortcuts

---
 .emacs | 39 ++++++++++++++++++++++++++++++++++++++-
 1 file changed, 38 insertions(+), 1 deletion(-)

(limited to '.emacs')

diff --git a/.emacs b/.emacs
index de86cb2..75995f0 100644
--- a/.emacs
+++ b/.emacs
@@ -33,6 +33,42 @@
  '(indent-tabs-mode nil)
  '(isar-display:show-main-goal t)
  '(isar-maths-menu-enable t)
+ '(isar-symbol-shortcuts (quote (("\\/" . "\\<or>") ("/\\" . "\\<and>") ("+O" . "\\<oplus>") ("-O" . "\\<ominus>") ("xO" . "\\<otimes>") ("/O" . "\\<oslash>") (".O" . "\\<odot>") ("|+" . "\\<dagger>") ("|++" . "\\<ddagger>") ("<=" . "\\<le>") ("|-" . "\\<turnstile>") (">=" . "\\<ge>") ("-|" . "\\<stileturn>") ("||" . "\\<parallel>") ("==" . "\\<equiv>") ("~=" . "\\<noteq>") ("~:" . "\\<notin>") ("~~~" . "\\<notapprox>") ("~~" . "\\<approx>") ("~==" . "\\<cong>") ("|<>|" . "\\<bowtie>") ("|=" . "\\<Turnstile>") ("=." . "\\<doteq>") ("_|_" . "\\<bottom>") ("</" . "\\<notle>") ("~>=" . "\\<notge>") ("==/" . "\\<notequiv>") ("~/" . "\\<notsim>") ("~=/" . "\\<notsimeq>") ("~~/" . "\\<notsimeq>") ("<-" . "\\<leftarrow>") ("<=" . "\\<Leftarrow>") ("->" . "\\<rightarrow>") ("=>" . "\\<Rightarrow>") ("<->" . "\\<leftrightarrow>") ("<=>" . "\\<Leftrightarrow>") ("|->" . "\\<mapsto>") ("<--" . "\\<longleftarrow>") ("<==" . "\\<Longleftarrow>") ("-->" . "\\<longrightarrow>") ("==>" . "\\<Longrightarrow>") ("<==>" . "\\<Longleftrightarrow>") ("|-->" . "\\<longmapsto>") ("<->" . "\\<longleftrightarrow>") ("<<" . "\\<guillemotleft>") (">>" . "\\<guillemotright>") ("<>" . "\\<diamond>") ("[|" . "\\<lbrakk>") ("|]" . "\\<rbrakk>") ("{|" . "\\<lbrace>") ("|}" . "\\<rbrace>") ("(|" . "\\<lparr>") ("|)" . "\\<rparr>") ("ALL" . "\\<forall>") ("EX" . "\\<exists>") ("!!" . "\\<And>") ("<|" . "\\<triangleleft>") 
+    ("<-->" . "\\<longleftrightarrow>") 
+    ("\\sse" . "\\<subseteq>") ("\\ess" . "\\<supseteq>") 
+    ("\\|" . "\\<^isub>") 
+    ("/|" . "\\<^isup>") 
+    ("\\a" . "\\<alpha>")
+    ("\\b" . "\\<beta>")
+    ("\\c" . "\\<chi>")
+    ("\\d" . "\\<delta>")
+    ("\\D" . "\\<Delta>")
+    ("\\e" . "\\<epsilon>")
+    ("\\f" . "\\<phi>")
+    ("\\F" . "\\<Phi>")
+    ("\\g" . "\\<gamma>")
+    ("\\G" . "\\<Gamma>")
+    ("\\i" . "\\<iota>")
+    ("\\k" . "\\<kappa>")
+    ("\\l" . "\\<lambda>")
+    ("\\L" . "\\<Lambda>")
+    ("\\m" . "\\<mu>")
+    ("\\n" . "\\<nu>")
+    ("\\o" . "\\<omega>")
+    ("\\O" . "\\<Omega>")
+    ("\\P" . "\\<Pi>")
+    ("\\p" . "\\<pi>")
+    ("\\q" . "\\<psi>")
+    ("\\Q" . "\\<Psi>")
+    ("\\r" . "\\<rho>")
+    ("\\R" . "\\<Rho>")
+    ("\\s" . "\\<sigma>") 
+    ("\\S" . "\\<Sigma>")
+    ("\\t" . "\\<tau>")
+    ("\\x" . "\\<xi>")
+    ("\\X" . "\\<Xi>")
+    ("\\z" . "\\<zeta>")
+)))
  '(isar-tracing:auto-try nil)
  '(isar-unicode-tokens-enable t)
  '(isar-unicode-tokens2-enable t)
@@ -57,4 +93,5 @@
  '(proof-highlight-dependency-face ((((type x) (class color) (background dark)) (:background "peru" :foreground "black"))))
  '(proof-highlight-dependent-face ((((type x) (class color) (background dark)) (:background "darkorange" :foreground "black"))))
  '(proof-region-mouse-highlight-face ((((type x) (class color) (background dark)) (:background "yellow3" :foreground "black"))))
- '(proof-warning-face ((((type x) (class color) (background dark)) (:background "orange2" :foreground "black")))))
+ '(proof-warning-face ((((type x) (class color) (background dark)) (:background "orange2" :foreground "black"))))
+ '(unicode-tokens-symbol-font-face ((t (:slant normal :weight normal :height 113 :width normal :foundry "unknown" :family "DejaVu Sans Mono")))))
-- 
cgit v1.2.3