657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\ProvidesPackage{hetcasl}[2002/10/04 v0.1 LaTeX Package for CASL v1.0.1]

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\NeedsTeXFormat{LaTeX2e}

5f5d1b4cc970b7f06ff8ef6526128e9a27303d88nd

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd% Required packages

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\RequirePackage{ifthen}

db479b48bd4d75423ed4a45e15b75089d1a8ad72fielding\RequirePackage{tabularx}

db479b48bd4d75423ed4a45e15b75089d1a8ad72fielding\RequirePackage{calc}

db479b48bd4d75423ed4a45e15b75089d1a8ad72fielding\RequirePackage[latin1]{inputenc}

db479b48bd4d75423ed4a45e15b75089d1a8ad72fielding\RequirePackage{xspace}

db479b48bd4d75423ed4a45e15b75089d1a8ad72fielding\RequirePackage{latexsym}

db479b48bd4d75423ed4a45e15b75089d1a8ad72fielding

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\newcounter{@opentabulars}

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\setcounter{@opentabulars}{0}

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\newlength{\@oldparindent}

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\newlength{\@hetcaslmaxwidth}

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\newlength{\@remhetcaslwidth}

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\newlength{\@KWwidth}%

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd% The next two length variables will be used in \KW

a2aaf7ab27f61d67535479c4fb3720a3d9255010nd\newlength{\@realWidth}\newlength{\@neededWidth}

7db9f691a00ead175b03335457ca296a33ddf31bnd

3577f1d38e53397f6b431c02011f875316b2f070nd\newif\ifhetcasl \hetcaslfalse

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newenvironment{hetcasl}[1][\textwidth]%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{%begin stuff

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\ifhetcasl%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\PackageError{hetcasl evironments cannot nested}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\else\hetcasltrue\fi%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\begingroup%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\setlength{\@oldparindent}{\the\parindent}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\setlength{\parindent}{0cm}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\setlength{\@hetcaslmaxwidth}{#1}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\setlength{\@remhetcaslwidth}{\the\@hetcaslmaxwidth}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%\begin{alltt}\begingroup\rmfamily

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\begin{tabbing}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% a little line to set up three useful tabstops for rendering parts

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% of a library and or specification

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\KW{view} \=\KW{preds} \=~~~~~~~\=\kill

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{%end stuff

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\end{tabbing}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%\endgroup\end{alltt}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%\@CloseAllTabulars%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\setlength{\parindent}{\the\@oldparindent}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\endgroup%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\hetcaslfalse%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\@HetCASLPrelude}{% HetCASL-Prelude

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\settowidth{\@KWwidth}{\textbf{view}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%%%% define all the makros needed for typesetting hetCASL

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% \KW prints a KeyWord within a box that is at least \@KWwidth wide.

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% If the keyword needs more space the box is as wide as the kyeword

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% is. The optional argument overrides \@KWwidth with the width of the

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% mandatory argument in bold face. The mandatory argument is always

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% printed in bold face.

41c470178723410705efade9f34436c78602db92jsl\newcommand{\KW}[2][no--format--keyword]%

41c470178723410705efade9f34436c78602db92jsl{\ifthenelse{\equal{##1}{no--format--keyword}}%

41c470178723410705efade9f34436c78602db92jsl{% no optional argument

41c470178723410705efade9f34436c78602db92jsl\settowidth{\@neededWidth}{\textbf{##2}}}%

41c470178723410705efade9f34436c78602db92jsl{% optional argument given

41c470178723410705efade9f34436c78602db92jsl\settowidth{\@realWidth}{\textbf{##2}}%

41c470178723410705efade9f34436c78602db92jsl\settowidth{\@KWwidth}{\textbf{##1}}%

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\ifthenelse{\@KWwidth > \@realWidth}%

41c470178723410705efade9f34436c78602db92jsl{\setlength{\@neededWidth}{\@KWwidth}}%

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh{\setlength{\@neededWidth}{\@realWidth}}}%

41c470178723410705efade9f34436c78602db92jsl\makebox[% set the width of the box not smaller

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% than the width of the KeyWord

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\@neededWidth]%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen[l]{\textbf{##2}}%

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% \SId prints its argument in small caps as a Structured Id for names

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% of specifications, views and libraries

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\SId}[1]{\textsc{##1}}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% \SIdIndex prints its argument like \SId but sets an Index Entry if

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% redifined

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\SIdIndex}[1]{\SId{##1}}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% \Id prints its argument in italic face as one word, for all other

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% identifiers not covered by \SId and only containing letters, numbers

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd% and \_

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\Id}[1]{\textit{##1}}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% \AX prints its argument in math modus

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\Ax}[1]{\ensuremath{##1}}%

c3c937a1510d6ff9cfa28ef3713e787f0e1a39c9coar

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\ANNOTEWORD}[1]{{\small{}\KW{\%##1}}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd%%%%% Heng todo:

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%% Makros aus casl.sty definieren

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\LBRACE} {\{}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\RBRACE} {\}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\FREE} {\KW{free}\xspace} %plain_keyword

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\FREELBRACE} {\FREE~\LBRACE}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\GENERATED} {\KW{generated}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd% \newcommand{\TYPE} {\KW{type}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd% \newcommand{\TYPES} {\KW{types}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\FREETYPE} {\FREE~\TYPE\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\FREETYPES} {\FREE~\TYPES\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\GENERATEDTYPE} {\GENERATED~\TYPE\xspace} %{\KW{generated~type}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\GENERATEDTYPES} {\GENERATED~\TYPES\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\VARS} {\KW{vars}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\AXIOM} {\KW{axiom}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\AXIOMS} {\KW{axioms}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\HIDE} {\KW{hide}\xspace}

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim\newcommand{\REVEAL} {\KW{reveal}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\WITH} {\KW{with}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\THEN} {\KW[view]{then}\xspace} % hetcasl_keyword

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\THENCONS} {\THEN~\ANNOTEWORD{cons}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\THENDEF} {\THEN~\ANNOTEWORD{def}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\THENIMPLIES} {\THEN~\ANNOTEWORD{implies}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\THENMONO} {\THEN~\ANNOTEWORD{mono}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\AND} {\KW{and}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\LOCAL} {\KW{local}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\THENLOCAL} {\THEN~\LOCAL}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\WITHIN} {\KW{within}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\CLOSED} {\KW{closed}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\FIT} {\KW{fit}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\TO} {\KW{to}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\LOGIC} {\KW{logic}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim\newcommand{\SPEC} {\KW[view]{spec}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\VIEW} {\KW[view]{view}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\END} {\KW{end}\xspace}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\ARCH} {\KW{arch}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\ARCHSPEC} {\ARCH~\KW{spec}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\UNITSPEC} {\KW{unit}~\KW{spec}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\UNITS} {\KW{units}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\GIVEN} {\KW{given}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\RESULT} {\KW{result}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\LIBRARY} {\KW{library}\xspace}

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim\newcommand{\FROM} {\KW[view]{from}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\GET} {\KW{get}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\VERSION} {\KW{version}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\PROD} {\Ax{\times}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\TOTAL} {\Ax{\rightarrow}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\PARTIAL} {\Ax{\rightarrow}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\MAPSTO} {\Ax{\mapsto}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\ASSOC} {\Id{assoc}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\COMM} {\Id{comm}}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\IDEM} {\Id{idem}}

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar\newcommand{\UNIT} {\Id{unit}\xspace}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\EXISTS} {\Ax{\exists}}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\EXISTSUNIQUE} {\AX{\exists!}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\IMPLIES} {\Ax{\Rightarrow}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\IFF} {\Ax{\Leftrightarrow}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\EEQ} {\Ax{\stackrel{e}{=}}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\A} {\Ax{\wedge}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\V} {\Ax{\vee}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\IN} {\Ax{\in}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\NOT} {\Ax{\neg}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\FORALL} {\Ax{\forall}}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\BULLET} {\Ax{\;\bullet\;}}

db389010adae4654ddb449076188715b4fb6bb08slive

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\IF} {\Id{if}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\WHEN} {\Id{when}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\ELSE} {\Id{else}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\DEF} {\Id{def}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\VAR} {\Id{var}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\AS} {\Id{as}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\TRUE} {\Id{true}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\FALSE} {\Id{false}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive

db389010adae4654ddb449076188715b4fb6bb08slive%%%% SORT, OP, PRED : drei Varianten %% Type auch

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\KWC}[2][preds]{%

db389010adae4654ddb449076188715b4fb6bb08slive\ifthenelse{\equal{##1}{KW}}%

db389010adae4654ddb449076188715b4fb6bb08slive{%KW as parameter

db389010adae4654ddb449076188715b4fb6bb08slive\KW{##2}}%

db389010adae4654ddb449076188715b4fb6bb08slive{% else to KW as parameter

db389010adae4654ddb449076188715b4fb6bb08slive\ifthenelse{\equal{##1}{ID}}%

db389010adae4654ddb449076188715b4fb6bb08slive{%ID as parameter

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\Id{##2}}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh{% else to ID as parameter

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar\KW[preds]{##2}}}%

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh}%% end of KWC definition

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\SORT}[1][preds]{\KWC[##1]{sort}\xspace}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\SORTS}[1][preds]{\KWC[##1]{sorts}\xspace}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh\newcommand{\OP}[1][preds]{\KWC[##1]{op}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\OPS}[1][preds]{\KWC[##1]{ops}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\PRED}[1][preds]{\KWC[##1]{pred}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\PREDS}[1][preds]{\KWC[##1]{preds}\xspace}

db389010adae4654ddb449076188715b4fb6bb08slive\newcommand{\TYPE}[1][preds]{\KWC[##1]{type}\xspace}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\TYPES}[1][preds]{\KWC[##1]{type}\xspace}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh

1f1b6bf13313fdd14a45e52e553d3ff28689b717coar%% 1. mit \KWC[preds]{} default

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh%% 2. mit \KWC[KW]{}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh%% 3. mit \KWC[ID]{}

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh

64801812c8979d4aad0631c5c614e54498fa5ebfhumbedooh%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% starting a library

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\library}[1]{\KW{library}\ \SId{##1}\ }

db389010adae4654ddb449076188715b4fb6bb08slive% printing a version number

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%\newcommand{\version}[1]{\KW{version}\ ##1}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% comments, annotations and labels

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\commentline}[1]{\textbf{\%\%}{\small##1}}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newenvironment{commentgroup}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{\textbf{\%\{}\begingroup\small}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{\endgroup\textbf{\}\%}}%

c14037646789087319802aaada2e8534ccab0158slive%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\annoteline}[2]{\textbf{\%##1}\ {\small \(##2\)}}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newenvironment{annotegroup}[1]%

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd{\textbf{\%##1(}\begingroup\small}%

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd{\endgroup\textbf{)\%}}%

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\casllabel}[1]{\textbf{\%(}{\small##1}\textbf{)\%}}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newenvironment{mlabel}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{\textbf{\%(}\begingroup\small}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{\endgroup\textbf{)\%}}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\place}{\_\_}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%% download items (from, get are automatically printed)

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newenvironment{downloaditem}[1]%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{\begingroup\sc

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\textnormal{\textbf{from}}\ ##1\ %

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%\textnormal{\ifthenelse{\equal{##1}{no-version}}{}{\version{##1}\ }}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\textnormal{\textbf{get}}}%

860b4efe27e7c1c9a2bf5c872b29c90f76849b51jim{\endgroup}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%% specifications

9f7a52b5d56d5fd29abe26843e50a1fbd427a09bhumbedooh% specdefn starts a new spec defn

9f7a52b5d56d5fd29abe26843e50a1fbd427a09bhumbedooh% arguments: ##1 ::= opt. semantic-anno

563512a0e3260268e86e205705c70bc3240fd3bbrbowen% ##2 ::= spec name

9f7a52b5d56d5fd29abe26843e50a1fbd427a09bhumbedooh% ##3 ::= parameters (see parameterspecs-env)

9f7a52b5d56d5fd29abe26843e50a1fbd427a09bhumbedooh% ##4 ::= imports (see importspecs-env)

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newenvironment{specdefn}[4][no-semantic-anno]%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{\textbf{spec}\ \textsc{##2}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\ifthenelse{\equal{##3}{}}{}{##3}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\ \(=\)%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen}%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen{}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% end of \@HetCASLPrelude

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\@HetCASLPrelude%

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%% helpers

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd% calculate a new width based on \@remhetcaslwidth and the fixed width

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen% given as argument.

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\@calc@width}[1]{}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen%\newcommand{\@tabnewline}{\\&}

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen

657ff8f1f85b30f62c39c7b89b8a66bf85a93a99rbowen\newcommand{\@condEOL}{\ifthenelse{\the@opentabulars=0}{\\}{\@tabnewline}}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd\newcommand{\@CloseAllTabulars}{}

210685ed32e07bffeaaa97dcb5e3a70ebd087fe5nd