1 % logics.sty : Logics Manuals Page Layout |
|
2 % |
|
3 \typeout{Document Style logics. Released 18 August 2003} |
|
4 |
|
5 \hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly} |
|
6 \hyphenation{data-type data-types co-data-type co-data-types } |
|
7 |
|
8 %usage: \iflabelundefined{LABEL}{if not defined}{if defined} |
|
9 \newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}} |
|
10 |
|
11 |
|
12 %%%INDEXING use isa-index to process the index |
|
13 |
|
14 \newcommand\seealso[2]{\emph{see also} #1} |
|
15 \usepackage{makeidx} |
|
16 |
|
17 %index, putting page numbers of definitions in boldface |
|
18 \def\bold#1{\textbf{#1}} |
|
19 \newcommand\fnote[1]{#1n} |
|
20 \newcommand\indexbold[1]{\index{#1|bold}} |
|
21 |
|
22 % The alternative to \protect\isa in the indexing macros is |
|
23 % \noexpand\noexpand \noexpand\isa |
|
24 % need TWO levels of \noexpand to delay the expansion of \isa: |
|
25 % the \noexpand\noexpand will leave one \noexpand, to be given to the |
|
26 % (still unexpanded) \isa token. See TeX by Topic, page 122. |
|
27 |
|
28 %%%% for indexing constants, symbols, theorems, ... |
|
29 \newcommand\cdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (constant)}} |
|
30 \newcommand\sdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (symbol)}} |
|
31 |
|
32 \newcommand\tdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)}} |
|
33 \newcommand\tdxbold[1]{\isa{#1}\index{#1@\protect\isa{#1} (theorem)|bold}} |
|
34 |
|
35 \newcommand\cldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (class)}} |
|
36 \newcommand\tydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (type)}} |
|
37 \newcommand\thydx[1]{\isa{#1}\index{#1@\protect\isa{#1} (theory)}} |
|
38 |
|
39 \newcommand\attrdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (attribute)}} |
|
40 \newcommand\cmmdx[1]{\index{#1@\protect\isacommand{#1} (command)}} |
|
41 \newcommand\commdx[1]{\isacommand{#1}\index{#1@\protect\isacommand{#1} (command)}} |
|
42 \newcommand\methdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (method)}} |
|
43 \newcommand\tooldx[1]{\isa{#1}\index{#1@\protect\isa{#1} (tool)}} |
|
44 \newcommand\settdx[1]{\isa{#1}\index{#1@\protect\isa{#1} (setting)}} |
|
45 |
|
46 %set argument in \bf font and index in ROMAN font (for definitions in text!) |
|
47 \newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@} |
|
48 |
|
49 \newcommand\rmindex[1]{{#1}\index{#1}\@} |
|
50 \newcommand\ttindex[1]{\texttt{#1}\index{#1@\texttt{#1}}\@} |
|
51 \newcommand\ttindexbold[1]{\texttt{#1}\index{#1@\texttt{#1}|bold}\@} |
|
52 |
|
53 \newcommand{\indexboldpos}[2]{#1\@} |
|
54 \newcommand{\ttindexboldpos}[2]{\isa{#1}\@} |
|
55 |
|
56 %\newtheorem{theorem}{Theorem}[section] |
|
57 \newtheorem{Exercise}{Exercise}[section] |
|
58 \newenvironment{exercise}{\begin{Exercise}\rm}{\end{Exercise}} |
|
59 \newcommand{\ttlbr}{\texttt{[|}} |
|
60 \newcommand{\ttrbr}{\texttt{|]}} |
|
61 \newcommand{\ttor}{\texttt{|}} |
|
62 \newcommand{\ttall}{\texttt{!}} |
|
63 \newcommand{\ttuniquex}{\texttt{?!}} |
|
64 \newcommand{\ttEXU}{\texttt{EX!}} |
|
65 \newcommand{\ttAnd}{\texttt{!!}} |
|
66 |
|
67 \newcommand{\isasymignore}{} |
|
68 \newcommand{\isasymimp}{\isasymlongrightarrow} |
|
69 \newcommand{\isasymImp}{\isasymLongrightarrow} |
|
70 \newcommand{\isasymFun}{\isasymRightarrow} |
|
71 \newcommand{\isasymuniqex}{\isamath{\exists!\,}} |
|
72 \renewcommand{\S}{Sect.\ts} |
|
73 |
|
74 \renewenvironment{isamarkuptxt}{\begin{isamarkuptext}}{\end{isamarkuptext}} |
|
75 |
|
76 \newif\ifremarks |
|
77 \newcommand{\REMARK}[1]{\ifremarks\marginpar{\raggedright\footnotesize#1}\fi} |
|
78 |
|
79 %names of Isabelle rules |
|
80 \newcommand{\rulename}[1]{\hfill(#1)} |
|
81 \newcommand{\rulenamedx}[1]{\hfill(#1\index{#1@\protect\isa{#1} (theorem)|bold})} |
|
82 |
|
83 %%%% meta-logical connectives |
|
84 |
|
85 \let\Forall=\bigwedge |
|
86 \let\Imp=\Longrightarrow |
|
87 \let\To=\Rightarrow |
|
88 \newcommand{\Var}[1]{{?\!#1}} |
|
89 |
|
90 %%% underscores as ordinary characters, not for subscripting |
|
91 %% use @ or \sb for subscripting; use \at for @ |
|
92 %% only works in \tt font |
|
93 %% must not make _ an active char; would make \ttindex fail! |
|
94 \gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other} |
|
95 \gdef\underscoreon{\catcode`\_=8\makeatother} |
|
96 \chardef\other=12 |
|
97 \chardef\at=`\@ |
|
98 |
|
99 % alternative underscore |
|
100 \def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em} |
|
101 |
|
102 |
|
103 %%%% ``WARNING'' environment |
|
104 \def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}} |
|
105 \newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 |
|
106 \small %%WAS\baselineskip=0.9\baselineskip |
|
107 \noindent \hangindent\parindent \hangafter=-2 |
|
108 \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}% |
|
109 {\par\endgroup\medbreak} |
|
110 |
|
111 |
|
112 %%%% Standard logical symbols |
|
113 \let\turn=\vdash |
|
114 \let\conj=\wedge |
|
115 \let\disj=\vee |
|
116 \let\imp=\rightarrow |
|
117 \let\bimp=\leftrightarrow |
|
118 \newcommand\all[1]{\forall#1.} %quantification |
|
119 \newcommand\ex[1]{\exists#1.} |
|
120 \newcommand{\pair}[1]{\langle#1\rangle} |
|
121 |
|
122 \newcommand{\lparr}{\mathopen{(\!|}} |
|
123 \newcommand{\rparr}{\mathclose{|\!)}} |
|
124 \newcommand{\fs}{\mathpunct{,\,}} |
|
125 \newcommand{\ty}{\mathrel{::}} |
|
126 \newcommand{\asn}{\mathrel{:=}} |
|
127 \newcommand{\more}{\ldots} |
|
128 \newcommand{\record}[1]{\lparr #1 \rparr} |
|
129 \newcommand{\dtt}{\mathord.} |
|
130 |
|
131 \newcommand\lbrakk{\mathopen{[\![}} |
|
132 \newcommand\rbrakk{\mathclose{]\!]}} |
|
133 \newcommand\List[1]{\lbrakk#1\rbrakk} %was \obj |
|
134 \newcommand\vpile[1]{\begin{array}{c}#1\end{array}} |
|
135 \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]} |
|
136 \newcommand{\Text}[1]{\mbox{#1}} |
|
137 |
|
138 \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D} |
|
139 \newcommand{\dsh}{\mathit{\dshsym}} |
|
140 |
|
141 \let\int=\cap |
|
142 \let\un=\cup |
|
143 \let\inter=\bigcap |
|
144 \let\union=\bigcup |
|
145 |
|
146 \def\ML{{\sc ml}} |
|
147 \def\AST{{\sc ast}} |
|
148 |
|
149 %macros to change the treatment of symbols |
|
150 \def\relsemicolon{\mathcode`\;="303B} %treat ; like a relation |
|
151 \def\binperiod{\mathcode`\.="213A} %treat . like a binary operator |
|
152 \def\binvert{\mathcode`\|="226A} %treat | like a binary operator |
|
153 |
|
154 %redefinition of \sloppy and \fussy to use \emergencystretch |
|
155 \def\sloppy{\tolerance2000 \hfuzz.5pt \vfuzz.5pt \emergencystretch=15pt} |
|
156 \def\fussy{\tolerance200 \hfuzz.1pt \vfuzz.1pt \emergencystretch=0pt} |
|
157 |
|
158 %non-bf version of description |
|
159 \def\descrlabel#1{\hspace\labelsep #1} |
|
160 \def\descr{\list{}{\labelwidth\z@ \itemindent-\leftmargin\let\makelabel\descrlabel}} |
|
161 \let\enddescr\endlist |
|
162 |
|
163 % The mathcodes for the letters A, ..., Z, a, ..., z are changed to |
|
164 % generate text italic rather than math italic by default. This makes |
|
165 % multi-letter identifiers look better. The mathcode for character c |
|
166 % is set to |"7000| (variable family) + |"400| (text italic) + |c|. |
|
167 % |
|
168 \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% |
|
169 \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 |
|
170 \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 |
|
171 \advance\count0 by1 \advance\count1 by1 \repeat}} |
|
172 \@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} |
|
173 \@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} |
|
174 |
|
175 %%% \dquotes permits usage of "..." for \hbox{...} |
|
176 %%% also taken from under.sty |
|
177 {\catcode`\"=\active |
|
178 \gdef\dquotes{\catcode`\"=\active \let"=\@mathText}% |
|
179 \gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}} |
|
180 \def\mathTextFont{\frenchspacing\tt} |
|
181 \def\dquotesoff{\catcode`\"=\other} |
|