+ <!ENTITY path "<emphasis><link linkend='grammar.path'>path</link></emphasis>">
+ <!ENTITY proofscript "<emphasis><link linkend='grammar.proofscript'>proof-script</link></emphasis>">
+ <!ENTITY proofstep "<emphasis><link linkend='grammar.proofstep'>proof-step</link></emphasis>">
+ <!ENTITY tactic "<emphasis><link linkend='grammar.tactic'>tactic</link></emphasis>">
+ <!ENTITY LCFtactical "<emphasis><link linkend='grammar.LCFtactical'>LCF-tactical</link></emphasis>">
+ <!ENTITY qstring "<emphasis><link linkend='grammar.qstring'>qstring</link></emphasis>">
+ <!ENTITY interpretation "<emphasis><link linkend='grammar.interpretation'>interpretation</link></emphasis>">
+ <!ENTITY autoparams "<emphasis><link linkend='grammar.autoparams'>auto_params</link></emphasis>">