# HG changeset patch
# User wenzelm
# Date 976561917 -3600
# Node ID d3190c5a0e76d0d88316c954cc2ccdad270422cb
# Parent  66d093e2076ec6398b5306f63b59d9b995689c6d
"translations": allow harpoons;

diff -r 66d093e2076e -r d3190c5a0e76 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Dec 11 20:11:11 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Dec 11 20:11:57 2000 +0100
@@ -152,8 +152,11 @@
 
 fun trans_arrow toks =
   (P.$$$ "=>" >> K Syntax.ParseRule ||
+    P.$$$ "\\<rightharpoonup>" >> K Syntax.ParseRule ||
     P.$$$ "<=" >> K Syntax.PrintRule ||
-    P.$$$ "==" >> K Syntax.ParsePrintRule) toks;
+    P.$$$ "\\<leftharpoondown>" >> K Syntax.PrintRule ||
+    P.$$$ "==" >> K Syntax.ParsePrintRule ||
+    P.$$$ "\\<rightleftharpoons>" >> K Syntax.ParsePrintRule) toks;
 
 val trans_line =
   trans_pat -- P.!!! (trans_arrow -- trans_pat)
@@ -667,7 +670,8 @@
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
-  "files", "in", "infixl", "infixr", "is", "output", "overloaded", "|"];
+  "files", "in", "infixl", "infixr", "is", "output", "overloaded", "|",
+  "\\<rightharpoonup>", "\\<leftharpoondown>", "\\<rightleftharpoons>"];
 
 val parsers = [
   (*theory structure*)