"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 define pyk of propositional calculus as text "propositional calculus" end text end define end math
end "
"
begin math define statement of propositional theory as all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var b end metavar imply metavar var c end metavar imply metavar var d end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var b end metavar imply metavar var d end metavar rule plus all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var c end metavar rule plus all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar imply metavar var c end metavar imply metavar var b end metavar rule plus all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var c end metavar imply not metavar var b end metavar imply not metavar var c end metavar imply metavar var b end metavar imply metavar var c end metavar end define end math
end "
\tex{ "
begin math define tex of propositional theory as text "T_{PC}" end text end define end math
end " }
"
begin math define pyk of propositional theory as text "propositional theory" end text end define end math
end "
"
begin math define pyk of var x imply var y as text "* imply *" end text end define end math
end "
\tex{ "
begin math define tex of var x imply var y as text "#1.
\Rightarrow #2." end text end define end math
end " }
"
begin math define value of 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 define pyk of axiom one as text "axiom one" end text end define end math
end "
\tex{ "
begin math define tex of axiom one as text "A1" end text end define end math
end " }
"
begin math define pyk of axiom two as text "axiom two" end text end define end math
end "
\tex{ "
begin math define tex of axiom two as text "A2" end text end define end math
end " }
"
begin math define pyk of axiom three as text "axiom three" end text end define end math
end "
\tex{ "
begin math define tex of axiom three as text "A3" end text end define end math
end " }
"
begin math define pyk of mp as text "mp" end text end define end math
end "
\tex{ "
begin math define tex of mp as text "MP" end text end define end math
end " }
"
begin math define statement of axiom one as propositional theory infer all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar imply metavar var c end metavar imply metavar var b end metavar end define
then define proof of axiom one as rule tactic end define end math
end "
"
begin math define statement of axiom two as propositional theory infer all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var d end metavar indeed metavar var b end metavar imply metavar var c end metavar imply metavar var d end metavar imply metavar var b end metavar imply metavar var c end metavar imply metavar var b end metavar imply metavar var d end metavar end define
then define proof of axiom two as rule tactic end define end math
end "
"
begin math define statement of axiom three as propositional theory infer all metavar var b end metavar indeed all metavar var c end metavar indeed not metavar var c end metavar imply not metavar var b end metavar imply not metavar var c end metavar imply metavar var b end metavar imply metavar var c end metavar end define
then define proof of axiom three as rule tactic end define end math
end "
"
begin math define statement of mp as propositional theory infer all metavar var b end metavar indeed all metavar var c end metavar indeed metavar var b end metavar infer metavar var b end metavar imply metavar var c end metavar infer metavar var c end metavar end define
then define proof of mp as rule tactic end define end math
end "
"
begin math define pyk of mendelson lemma one eight as text "mendelson lemma one eight" end text end define end math
end "
\tex{ "
begin math define tex of mendelson lemma one eight as text "LEMMA 1.8" end text end define end math
end " }
"
begin math define statement of mendelson lemma one eight as propositional theory infer all metavar var b end metavar indeed metavar var b end metavar imply metavar var b end metavar end define end math
end "
"
begin math define proof of mendelson lemma one eight as lambda var c dot lambda var x dot proof expand quote propositional theory infer all metavar var b end metavar indeed axiom two conclude metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar cut axiom one conclude metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar cut mp modus ponens metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar modus ponens metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar conclude metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar cut axiom one conclude metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar cut mp modus ponens metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar modus ponens metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar imply metavar var b end metavar conclude metavar var b end metavar imply metavar var b end metavar end quote state proof state cache var c end expand end define 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,