doc-src/isar.sty

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/isar.sty	Tue Jul 20 18:50:46 1999 +0200
@@ -0,0 +1,70 @@
+
+%% $Id$
+
+\usepackage{ifthen}
+
+%Isar language elements
+\newcommand{\I@keyword}[1]{{\mathord{\mathbf{#1}}}}
+\newcommand{\I@optname}[1]{\ifthenelse{\equal{}{#1}}{}{~#1\colon}}
+\newcommand{\I@optoptname}[1]{\ifthenelse{\equal{}{#1}}{}{~[#1\colon]}}
+\newcommand{\I@optmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~(#1)}}
+\newcommand{\I@optoptmeth}[1]{\ifthenelse{\equal{}{#1}}{}{~[(#1)]}}
+
+\newcommand{\LEMMANAME}{\I@keyword{lemma}}
+\newcommand{\THEOREMNAME}{\I@keyword{theorem}}
+\newcommand{\NOTENAME}{\I@keyword{note}}
+\newcommand{\FROMNAME}{\I@keyword{from}}
+\newcommand{\WITHNAME}{\I@keyword{with}}
+\newcommand{\FIXNAME}{\I@keyword{fix}}
+\newcommand{\ASSUMENAME}{\I@keyword{assume}}
+\newcommand{\PRESUMENAME}{\I@keyword{presume}}
+\newcommand{\HAVENAME}{\I@keyword{have}}
+\newcommand{\SHOWNAME}{\I@keyword{show}}
+\newcommand{\HENCENAME}{\I@keyword{hence}}
+\newcommand{\THUSNAME}{\I@keyword{thus}}
+\newcommand{\PROOFNAME}{\I@keyword{proof}}
+\newcommand{\QEDNAME}{\I@keyword{qed}}
+\newcommand{\BYNAME}{\I@keyword{by}}
+\newcommand{\ISNAME}{\I@keyword{is}}
+\newcommand{\CONCLNAME}{\I@keyword{concl}}
+\newcommand{\LETNAME}{\I@keyword{let}}
+\newcommand{\DEFNAME}{\I@keyword{def}}
+\newcommand{\SUFFNAME}{\I@keyword{suffient}}
+\newcommand{\CMTNAME}{\I@keyword{-{}-}}
+
+\newcommand{\TYPES}{\I@keyword{types}}
+\newcommand{\CONSTS}{\I@keyword{consts}}
+\newcommand{\DEFS}{\I@keyword{defs}}
+\newcommand{\NOTE}[2]{\NOTENAME~#1=#2}
+\newcommand{\FROM}[1]{\FROMNAME~#1}
+\newcommand{\WITH}[1]{\WITHNAME~#1}
+\newcommand{\FIX}[1]{\FIXNAME~#1}
+\newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2}
+\newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2}
+\newcommand{\THEN}{\I@keyword{then}}
+\newcommand{\BEGIN}{\I@keyword{begin}}
+\newcommand{\END}{\I@keyword{end}}
+\newcommand{\BG}{\lceil}
+\newcommand{\EN}{\rfloor}
+\newcommand{\HAVE}[2]{\I@keyword{have}\I@optname{#1}~#2}
+\newcommand{\SHOW}[2]{\I@keyword{show}\I@optname{#1}~#2}
+\newcommand{\HENCE}[2]{\I@keyword{hence}\I@optname{#1}~#2}
+\newcommand{\THUS}[2]{\I@keyword{thus}\I@optname{#1}~#2}
+\newcommand{\LEMMA}[2]{\LEMMANAME\I@optname{#1}~#2}
+\newcommand{\THEOREM}[2]{\THEOREMNAME\I@optname{#1}~#2}
+\newcommand{\PROOF}[1]{\PROOFNAME\I@optmeth{#1}}
+\newcommand{\PPROOF}[1]{\PPROOFNAME\I@optmeth{#1}}
+\newcommand{\QED}[1]{\QEDNAME\I@optmeth{#1}}
+\newcommand{\BY}[1]{\BYNAME\I@optmeth{#1}}
+\newcommand{\DOT}{\I@keyword{.}}
+\newcommand{\DDOT}{\I@keyword{.\,.}}
+\newcommand{\DDDOT}{\dots}
+\newcommand{\IS}[1]{(\ISNAME~#1)}
+\newcommand{\LET}[1]{\LETNAME~#1}
+\newcommand{\LETT}[1]{\LETNAME~#1\dt\;}
+\newcommand{\DEF}[2]{\DEFNAME\I@optname{#1}~#2}
+\newcommand{\SUFF}[1]{\SUFFNAME~#1}
+\newcommand{\ATT}[1]{\ap [#1]}
+\newcommand{\CMT}[1]{\CMTNAME~\text{#1}}
+\newcommand{\ALSO}{\I@keyword{also}}
+\newcommand{\FINALLY}{\I@keyword{finally}}