"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}
\usepackage[danish]{babel}
\begin {document}
"
begin math pyk define prop as "prop" end define end math
end "
% *********** Implikation *************
Forsoeg paa implikation:
\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 var y guard parenthesis x macro imply var y end parenthesis end define end math
end "
"
begin math pyk define var x imply var y as "* imply *" end define end math
end "
% ********** Den samlede teori ***************
Her er vores teori:
"
begin math tex define prop theory as "Propositional Calculus" end define end math
end "
"
begin math theory prop theory end theory end math
end "
"
begin math pyk define prop theory as "prop theory" end define end math
end "
Vi forsoeger at definere axiom 1:
% ****** Axiom 1 ******
"
begin math tex define axiom one as "A1" end define end math
end "
"
begin math in theory prop 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 pyk define axiom one as "axiom one" end define end math
end "
Saa er turen kommet til axiom 2:
% ******* Axiom 2 *****
"
begin math tex define axiom two as "A2" end define end math
end "
"
begin math in theory prop 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 pyk define axiom two as "axiom two" end define end math
end "
% ******** Axiom 3 *************
Efter aksiom 2 kommer aksiom 3:
"
begin math tex define axiom three as "A3" end define end math
end "
"
begin math in theory prop 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 pyk define axiom three as "axiom three" end define end math
end "
% ********* Modus Ponens ****************
Saa definerer vi modus ponens...
"
begin math tex define mp as "MP" end define end math
end "
"
begin math in theory prop 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 mp as "mp" end define end math
end "
% *********** Det kaere lemma **************
Vi kan nu formelt udtrykke den paastand, at ethvert udsagn implicerer sig selv:
HVAD SKER DER HEEEEERR??????
"
begin math tex define auto imply as "AutoImply" end define end math
end "
"
begin math pyk define auto imply as "auto imply" end define end math
end " % claim succeeded hertil
"
begin math in theory prop theory lemma auto imply says all meta b indeed meta b imply meta b end lemma end math
end "
Saa langt saa godt...
"
begin math prop theory proof of auto imply reads arbitrary meta b cut line ell a because axiom one indeed meta b imply meta b imply meta b cut line ell b 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 c because axiom one indeed meta b imply parenthesis meta b imply meta b end parenthesis imply meta b cut line ell d because mp modus ponens ell c modus ponens ell b indeed parenthesis meta b imply meta b imply meta b end parenthesis imply meta b imply meta b cut because mp modus ponens ell a modus ponens ell d indeed meta b imply meta b qed end math
end "
% *** test ***
Tests:
"
begin math false test two plus three tagged equal seven end test end math
end "
\end{document}
End of file
latex page"
The pyk compiler, version 0.grue.20050502+ by Klaus Grue,