|Page 318 of 800||Search internet|
The following constructs allow to express the last line of a proof:
line L : A >> C ; line L : A >> C qed
The two constructs are identical except that the former is rendered with a terminating semicolon and the latter is rendered with a terminating box. The former is used in Line L07 and the latter in Line L10 of the multzero proof:
The line number L of end lines is purely decorative and is discarded during macro expansion.
|Page 318 of 800||Search logiweb.eu|