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