# HG changeset patch
# User wenzelm
# Date 964954869 -7200
# Node ID f778551af3edd613e3f61a1c68b2f7fd46c07802
# Parent  705ca49129fc50fa74eba675bca58704250eb059
'def': no constraint on variable;

diff -r 705ca49129fc -r f778551af3ed doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun Jul 30 12:56:14 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Sun Jul 30 13:01:09 2000 +0200
@@ -607,7 +607,7 @@
   ;
   ('assume' | 'presume') (assm comment? + 'and')
   ;
-  'def' thmdecl? \\ var '==' term termpat? comment?
+  'def' thmdecl? \\ name '==' term termpat? comment?
   ;
 
   var: name ('::' type)?