# HG changeset patch
# User wenzelm
# Date 976999408 -3600
# Node ID 4cf4bbc2526734d6fdfc02bf99b7b42c1a3a6de8
# Parent  c186279eecea889c8c79855b7aaee303c50036c4
'def': \<equiv>;

diff -r c186279eecea -r 4cf4bbc25267 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Dec 16 21:41:51 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 16 21:43:28 2000 +0100
@@ -151,12 +151,9 @@
   Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
 
 fun trans_arrow toks =
-  (P.$$$ "=>" >> K Syntax.ParseRule ||
-    P.$$$ "\\<rightharpoonup>" >> K Syntax.ParseRule ||
-    P.$$$ "<=" >> K Syntax.PrintRule ||
-    P.$$$ "\\<leftharpoondown>" >> K Syntax.PrintRule ||
-    P.$$$ "==" >> K Syntax.ParsePrintRule ||
-    P.$$$ "\\<rightleftharpoons>" >> K Syntax.ParsePrintRule) toks;
+  ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
+    (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
+    (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
 
 val trans_line =
   trans_pat -- P.!!! (trans_arrow -- trans_pat)
@@ -348,7 +345,7 @@
 
 val defP =
   OuterSyntax.command "def" "local definition" K.prf_asm
-    (P.opt_thm_name ":" -- (P.name -- (P.$$$ "==" |-- P.!!! P.termp))
+    (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))
       -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
 
 val fixP =
@@ -670,8 +667,9 @@
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
-  "files", "in", "infixl", "infixr", "is", "output", "overloaded", "|",
-  "\\<rightharpoonup>", "\\<leftharpoondown>", "\\<rightleftharpoons>"];
+  "files", "in", "infixl", "infixr", "is", "output", "overloaded",
+  "|", "\\<rightharpoonup>", "\\<leftharpoondown>",
+  "\\<rightleftharpoons>", "\\<equiv>"];
 
 val parsers = [
   (*theory structure*)