--- 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)?