From e1013ade602abd388a0c6cfdca72aaf41498c14e Mon Sep 17 00:00:00 2001
From: Makarius Wenzel <makarius@sketis.net>
Date: Mon, 7 Jul 2008 18:46:23 +0000
Subject: isar-shortcut-alist: map << >> to guillemots -- this is what
 HOL-Nominal expects;

---
 isar/isar-unicode-tokens.el | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'isar')

diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index 6c79224b..22a02e89 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -540,9 +540,9 @@ results will be undefined when files are saved."
     ("<==>" . "⟷")
     ("|-->" . "⟼")
     ("<-->" . "⟷")
-    ("<<" . "⟪")
+    ("<<" . "«")
     ("[|" . "⟦")
-    (">>" . "⟫")
+    (">>" . "»")
     ("|]" . "⟧")
 ;    ("``" . "”")
 ;    ("''" . "“")
-- 
cgit v1.2.3