--- a/doc-src/IsarRef/pure.tex Wed Nov 30 21:51:23 2005 +0100
+++ b/doc-src/IsarRef/pure.tex Wed Nov 30 22:52:46 2005 +0100
@@ -709,7 +709,9 @@
;
('assume' | 'presume') (props + 'and')
;
- 'def' thmdecl? \\ name ('==' | equiv) term termpat?
+ 'def' (def + 'and')
+ ;
+ def: thmdecl? \\ name ('==' | equiv) term termpat?
;
\end{rail}
@@ -733,7 +735,8 @@
``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'',
with the resulting hypothetical equation solved by reflexivity.
- The default name for the definitional equation is $x_def$.
+ The default name for the definitional equation is $x_def$. Several
+ simultaneous definitions may be given at the same time.
\end{descr}