# HG changeset patch
# User wenzelm
# Date 931766558 -7200
# Node ID 3ae2eeabde80a825c0a0930f0d7632e3e50c6c8a
# Parent  4a13e098ee86f83ddc2d3215f25d97f1f577f6f8
def: ==;

diff -r 4a13e098ee86 -r 3ae2eeabde80 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Jul 10 21:58:19 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jul 12 10:02:38 1999 +0200
@@ -310,7 +310,7 @@
 val defP =
   OuterSyntax.command "def" "local definition" K.prf_asm
     ((P.opt_thm_name ":" -- (P.name -- Scan.option (P.$$$ "::" |-- P.typ) --
-      (P.$$$ "=" |-- P.termp)) >> P.triple1) -- P.marg_comment
+      (P.$$$ "==" |-- P.termp)) >> P.triple1) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
 
 val fixP =