lstlangmizar.sty
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAFP4q157DZmHx+ZA=bqzg1QKvkK3thfatC6wLyE3XweVm7WZbA@mail.gmail.com> |
Hi,
at https://raw.github.com/JUrban/mizarmode/master/lstlangmizar.sty is
a basic LaTeX syntax highlighting mode for Mizar. Use it with Mizar
code in LaTeX like this:
\begin{lstlisting}[language=Mizar]
::$N Brouwer Fixed Point Theorem
theorem Th14:
for r being non negative (real number), o being Point of TOP-REAL 2,
f being continuous Function of Tdisk(o,r), Tdisk(o,r)
holds f has_a_fixpoint
proof ...
\end{lstlisting}
Josef