(custom-set-variables ;; custom-set-variables was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. '(fill-column 80) '(indent-tabs-mode nil) '(isar-display:show-main-goal t) '(isar-maths-menu-enable t) '(isar-proof:Sledgehammer:\ Time\ Limit 60) '(isar-symbol-shortcuts (quote (("\\/" . "\\") ("/\\" . "\\") ("+O" . "\\") ("-O" . "\\") ("xO" . "\\") ("/O" . "\\") (".O" . "\\") ("|+" . "\\") ("|++" . "\\") ("<=" . "\\") ("|-" . "\\") (">=" . "\\") ("-|" . "\\") ("||" . "\\") ("==" . "\\") ("~=" . "\\") ("~:" . "\\") ("~~~" . "\\") ("~~" . "\\") ("~==" . "\\") ("|<>|" . "\\") ("|=" . "\\") ("=." . "\\") ("_|_" . "\\") ("") ("~>=" . "\\") ("==/" . "\\") ("~/" . "\\") ("~=/" . "\\") ("~~/" . "\\") ("<-" . "\\") ("<=" . "\\") ("->" . "\\") ("=>" . "\\") ("<->" . "\\") ("<=>" . "\\") ("|->" . "\\") ("<--" . "\\") ("<==" . "\\") ("-->" . "\\") ("==>" . "\\") ("<==>" . "\\") ("|-->" . "\\") ("<->" . "\\") ("<<" . "\\") (">>" . "\\") ("<>" . "\\") ("[|" . "\\") ("|]" . "\\") ("{|" . "\\") ("|}" . "\\") ("(|" . "\\") ("|)" . "\\") ("ALL" . "\\") ("EX" . "\\") ("!!" . "\\") ("<|" . "\\") ("<-->" . "\\") ("\\sse" . "\\") ("\\ess" . "\\") ("\\\\" . "\\") ("\\|" . "\\<^sub>") ("|/" . "\\<^sub>") ("|\\" . "\\<^sup>") ("/|" . "\\<^sup>") ("\\a" . "\\") ("\\b" . "\\") ("\\c" . "\\") ("\\d" . "\\") ("\\D" . "\\") ("\\e" . "\\") ("\\f" . "\\") ("\\F" . "\\") ("\\g" . "\\") ("\\G" . "\\") ("\\i" . "\\") ("\\k" . "\\") ("\\l" . "\\") ("\\L" . "\\") ("\\m" . "\\") ("\\n" . "\\") ("\\o" . "\\") ("\\O" . "\\") ("\\P" . "\\") ("\\p" . "\\") ("\\q" . "\\") ("\\Q" . "\\") ("\\r" . "\\") ("\\R" . "\\") ("\\s" . "\\") ("\\S" . "\\") ("\\t" . "\\") ("\\x" . "\\") ("\\X" . "\\") ("\\z" . "\\") ("\\8" . "\\")))) '(isar-tracing:auto-quickcheck t) '(isar-tracing:auto-try nil) '(isar-unicode-tokens-enable t) '(isar-unicode-tokens2-enable t) '(isar-use-find-theorems-form nil) '(isar-x-symbol-enable nil) '(proof-delete-empty-windows nil) '(proof-imenu-enable t) '(proof-three-window-enable t) '(show-paren-mode t)) (custom-set-faces ;; custom-set-faces was added by Custom. ;; If you edit it by hand, you could mess it up, so be careful. ;; Your init file should contain only one such instance. ;; If there is more than one, they won't work right. '(column-enforce-face ((t (:underline "firebrick")))) '(isabelle-free-name-face ((((type x) (class color) (background dark)) (:foreground "lightblue")))) '(isabelle-quote-face ((t (:foreground "grey21")))) '(isabelle-string-face ((((type x) (class color) (background dark)) (:foreground "cyan3")))) '(isabelle-var-name-face ((((type x) (class color) (background dark)) (:foreground "lightblue3")))) '(linum ((t (:inherit (shadow default) :foreground "gold")))) '(proof-boring-face ((((type x) (class color) (background dark)) (:foreground "cyan3")))) '(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")))) '(region ((t (:background "dark slate gray")))) '(unicode-tokens-symbol-font-face ((t (:slant normal :weight normal :height 113 :width normal :foundry "unknown" :family "DejaVu Sans Mono")))))