# HG changeset patch
# User wenzelm
# Date 976999274 -3600
# Node ID 60c795d6bd9e3828bd813a9045dbb127f59f5f9b
# Parent  8cb1d80f10de03706b037be239eeb07be5e1450a
'def': equiv;

diff -r 8cb1d80f10de -r 60c795d6bd9e doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sat Dec 16 21:40:49 2000 +0100
+++ b/doc-src/IsarRef/pure.tex	Sat Dec 16 21:41:14 2000 +0100
@@ -612,12 +612,15 @@
 hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
 Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
 
+\railalias{equiv}{\isasymequiv}
+\railterm{equiv}
+
 \begin{rail}
   'fix' (vars + 'and') comment?
   ;
   ('assume' | 'presume') (assm comment? + 'and')
   ;
-  'def' thmdecl? \\ name '==' term termpat? comment?
+  'def' thmdecl? \\ name ('==' | equiv) term termpat? comment?
   ;
 
   var: name ('::' type)?