Library Directive

Syntax

Library-Directive   =  
 (   notation   |  
constructors   |  
clusters   |  
definitions   |  
theorems   |  
schemes   )   Article-Name   {   ,   Article-Name   }   ;   .
 
Article-Name   =   File-Name   .


See also

Home | Index of Syntax Items

Last modified: June 26, 2000