"File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
{\list{\@biblabel{\@arabic\c@enumiv}}%
{\settowidth\labelwidth{\@biblabel{#1}}%
\leftmargin\labelwidth
\advance\leftmargin\labelsep
\@openbib@code
\usecounter{enumiv}%
\let\p@enumiv\@empty
\renewcommand\theenumiv{\@arabic\c@enumiv}}%
\sloppy
\clubpenalty4000
\@clubpenalty \clubpenalty
\widowpenalty4000%
\sfcode`\.\@m}
{\def\@noitemerr
{\@latex@warning{Empty `thebibliography' environment}}%
\endlist}
End of file
File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}
\usepackage{latexsym}
%\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}
% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}
\usepackage{makeidx}
\usepackage{page}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}
\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=A Logiweb base page}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}
% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}
% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}
% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}
\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}
\afterheading}
\begin {document}
"
begin math pyk define propositional calculus as "propositional calculus" end define end math
end "
"
begin math theory propositional theory end theory end math
end "
\tex{ "
begin math tex define propositional theory as "T_{PC}" end define end math
end " }
"
begin math pyk define propositional theory as "propositional theory" end define end math
end "
"
begin math pyk define var x imply var y as "* imply *" end define end math
end "
\tex{ "
begin math tex define var x imply var y as "#1.
\Rightarrow #2." end define end math
end " }
"
begin math value define var x imply var y as not var x or var y end define end math
end "
"
begin math test true imply true end test end math
end "
"
begin math false test true imply false end test end math
end "
"
begin math test false imply true end test end math
end "
"
begin math test false imply false end test end math
end "
"
begin math pyk define axiom one as "axiom one" end define end math
end "
\tex{ "
begin math tex define axiom one as "A1" end define end math
end " }
"
begin math pyk define axiom two as "axiom two" end define end math
end "
\tex{ "
begin math tex define axiom two as "A2" end define end math
end " }
"
begin math pyk define axiom three as "axiom three" end define end math
end "
\tex{ "
begin math tex define axiom three as "A3" end define end math
end " }
"
begin math pyk define mp as "mp" end define end math
end "
\tex{ "
begin math tex define mp as "MP" end define end math
end " }
"
begin math in theory propositional theory rule axiom one says all meta b indeed all meta c indeed meta b imply meta c imply meta b end rule end math
end "
"
begin math in theory propositional theory rule axiom two says all meta b indeed all meta c indeed all meta d indeed parenthesis meta b imply meta c imply meta d end parenthesis imply parenthesis meta b imply meta c end parenthesis imply meta b imply meta d end rule end math
end "
"
begin math in theory propositional theory rule axiom three says all meta b indeed all meta c indeed parenthesis not meta c imply not meta b end parenthesis imply parenthesis not meta c imply meta b end parenthesis imply meta c end rule end math
end "
"
begin math in theory propositional theory rule mp says all meta b indeed all meta c indeed meta b infer meta b imply meta c infer meta c end rule end math
end "
"
begin math pyk define mendelson lemma one eight as "mendelson lemma one eight" end define end math
end "
\tex{ "
begin math tex define mendelson lemma one eight as "LEMMA 1.8" end define end math
end " }
"
begin math in theory propositional theory lemma mendelson lemma one eight says all meta b indeed meta b imply meta b end lemma end math
end "
"
begin math propositional theory proof of mendelson lemma one eight reads arbitrary meta b cut line ell a because axiom two indeed parenthesis meta b imply parenthesis meta b imply meta b end parenthesis imply meta b end parenthesis imply parenthesis meta b imply meta b imply meta b end parenthesis imply meta b imply meta b cut line ell b because axiom one indeed meta b imply parenthesis meta b imply meta b end parenthesis imply meta b cut line ell c because mp modus ponens ell b modus ponens ell a indeed parenthesis meta b imply meta b imply meta b end parenthesis imply meta b imply meta b cut line ell d because axiom one indeed meta b imply meta b imply meta b cut because mp modus ponens ell d modus ponens ell c indeed meta b imply meta b qed end math
end "
\appendix
\section{\TeX\ definitions}
\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outex
\input{./page.otx}
\end{list}
\end{document}
End of file
latex page"
The pyk compiler, version 0.grue.20050603 by Klaus Grue,