LP: \1<\/title>\ <\/head>\ <body>\ <h1>LP, the Larch Prover -- \1<\/h1>\ <hr>/ /\\head{$[0-9]$}{$[^{}]*$}/s//<h\1>\2<\/h\1>/ /^\\ref{/d /\\begin{itemize}/s//<ul>/ /\\end{itemize}/s//<\/ul>/ /\\begin{description}/s//<dl>/ /\\end{description}/s//<\/dl>/ /\\begin{verbatim}/{ s//<blockquote><pre><tt>/ N s/\n// } /\\end{verbatim}/s//<\/tt><\/pre><\/blockquote>/ /\\begin{quote}/s//<blockquote>/ /\\end{quote}/s//<\/blockquote>/ /\\item/s//<li>/ /\\dt/s//<dt>/ /\\dd/s//<dd>/ /\\[$]/s//$/g /\\%/s//%/g /\\lt/s//\</g /\\gt/s//\>/g /\\anchor{$[^{}]*$}/s//<a name="\1">/g /\\clink{$[^{}]*$}/s//<a href="..\/commands\/\1.html">\1<\/a>/g /\\cflink{$[^{}]*$}/s//<a href="..\/commands\/\1.html">\1<\/a>/g /\\dlink{$[^{}]*.lp$}{$[^{}]*$}/s//<a href="\1">\2<\/a>/g /\\dlink{$[^{}]*$}{$[^{}]*$}/s//<a href="\1.html">\2<\/a>/g /\\dflink{$[^{}]*.lp$}{$[^{}]*$}/s//<a href="\1">\2<\/a>/g /\\dflink{$[^{}]*$}{$[^{}]*$}/s//<a href="\1.html">\2<\/a>/g /\\glink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/glossary\/\1.html">\2<\/a>/g /\\llink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/logic\/\1.html">\2<\/a>/g /\\olink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/operation\/\1.html">\2<\/a>/g /\\plink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/proof\/\1.html">\2<\/a>/g /\\pflink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/proof\/\1.html"><tt>\2<\/tt><\/a>/g /\\slink{$[^{}]*$}{$[^{}]*$}/s//\<<a href="\1.html#\2">\2<\/a>\>/g /\\setlink{$[^{}]*$}/s//<a href="..\/settings\/\1.html">\1<\/a>/g /\\ftp{$[^{}]*$}/s??<a href="ftp://larch.lcs.mit.edu/pub/Larch/lp/\1">\1</a>?g /\\s{$[^{}]*$}/s//\<\1\>/g /\\sd{$[^{}]*$}/s//<a name="\1">\<\1\>/g /\\v{$[^{}]*$}/s//<var>\1<\/var>/g /\\def{$[^{}]*$}/s//<em>\1<\/em>/g /\\f{$[^{}]*$}/s//<tt>\1<\/tt>/g /\\fq{$[^{}]*$}/s//<tt>\1<\/tt>/g /\\qf{$[^{}]*$}/s//"<tt>\1<\/tt>"/g /\\f#$[^#]*$#/s//<tt>\1<\/tt>/g /\\fq#$[^#]*$#/s//<tt>\1<\/tt>/g /\\qf#$[^#]*$#/s//"<tt>\1<\/tt>"/g /\\v#$[^#]*$#/s//<var>\1<\/var>/g /\\p/s//<p>/ /\\br/s//<br>/g

/\\doc{$[^{}]*$}/s//\ \ LP: \1<\/title>\ <\/head>\ <body>\ <h1>LP, the Larch Prover -- \1<\/h1>\ <hr>/ /\\head{$[0-9]$}{$[^{}]*$}/s//<h\1>\2<\/h\1>/ /^\\ref{/d /\\begin{itemize}/s//<ul>/ /\\end{itemize}/s//<\/ul>/ /\\begin{description}/s//<dl>/ /\\end{description}/s//<\/dl>/ /\\begin{verbatim}/{ s//<blockquote><pre><tt>/ N s/\n// } /\\end{verbatim}/s//<\/tt><\/pre><\/blockquote>/ /\\begin{quote}/s//<blockquote>/ /\\end{quote}/s//<\/blockquote>/ /\\item/s//<li>/ /\\dt/s//<dt>/ /\\dd/s//<dd>/ /\\[$]/s//$/g /\\%/s//%/g /\\lt/s//\</g /\\gt/s//\>/g /\\anchor{$[^{}]*$}/s//<a name="\1">/g /\\clink{$[^{}]*$}/s//<a href="..\/commands\/\1.html">\1<\/a>/g /\\cflink{$[^{}]*$}/s//<a href="..\/commands\/\1.html">\1<\/a>/g /\\dlink{$[^{}]*.lp$}{$[^{}]*$}/s//<a href="\1">\2<\/a>/g /\\dlink{$[^{}]*$}{$[^{}]*$}/s//<a href="\1.html">\2<\/a>/g /\\dflink{$[^{}]*.lp$}{$[^{}]*$}/s//<a href="\1">\2<\/a>/g /\\dflink{$[^{}]*$}{$[^{}]*$}/s//<a href="\1.html">\2<\/a>/g /\\glink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/glossary\/\1.html">\2<\/a>/g /\\llink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/logic\/\1.html">\2<\/a>/g /\\olink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/operation\/\1.html">\2<\/a>/g /\\plink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/proof\/\1.html">\2<\/a>/g /\\pflink{$[^{}]*$}{$[^{}]*$}/s//<a href="..\/proof\/\1.html"><tt>\2<\/tt><\/a>/g /\\slink{$[^{}]*$}{$[^{}]*$}/s//\<<a href="\1.html#\2">\2<\/a>\>/g /\\setlink{$[^{}]*$}/s//<a href="..\/settings\/\1.html">\1<\/a>/g /\\ftp{$[^{}]*$}/s??<a href="ftp://larch.lcs.mit.edu/pub/Larch/lp/\1">\1</a>?g /\\s{$[^{}]*$}/s//\<\1\>/g /\\sd{$[^{}]*$}/s//<a name="\1">\<\1\>/g /\\v{$[^{}]*$}/s//<var>\1<\/var>/g /\\def{$[^{}]*$}/s//<em>\1<\/em>/g /\\f{$[^{}]*$}/s//<tt>\1<\/tt>/g /\\fq{$[^{}]*$}/s//<tt>\1<\/tt>/g /\\qf{$[^{}]*$}/s//"<tt>\1<\/tt>"/g /\\f#$[^#]*$#/s//<tt>\1<\/tt>/g /\\fq#$[^#]*$#/s//<tt>\1<\/tt>/g /\\qf#$[^#]*$#/s//"<tt>\1<\/tt>"/g /\\v#$[^#]*$#/s//<var>\1<\/var>/g /\\p/s//<p>/ /\\br/s//<br>/g