changeset 45701 | 615da8b8d758 |
parent 45678 | 1a6206f538d4 |
child 45758 | 6210c350d88b |
child 45767 | fe2fd2f76f48 |
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Nov 30 21:14:01 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Nov 30 23:30:08 2011 +0100 @@ -1036,10 +1036,6 @@ \rail@endplus \rail@end \rail@begin{2}{\isa{spec}} -\rail@bar -\rail@nextbar{1} -\rail@nont{\hyperlink{syntax.parname}{\mbox{\isa{parname}}}}[] -\rail@endbar \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[] \rail@bar \rail@nextbar{1}