|
1 %% |
|
2 %% $Id$ |
|
3 %% |
|
4 %% definitions of many Isabelle symbols |
|
5 %% |
|
6 |
|
7 \usepackage{latexsym} |
|
8 |
|
9 \newcommand{\bigsqcap}{\overline{|\,\,|}} %just a hack |
|
10 %\def\textbrokenbar??? etc |
|
11 |
|
12 \newcommand{\isasymspacespace}{~~} |
|
13 \newcommand{\isasymGamma}{$\Gamma$} |
|
14 \newcommand{\isasymDelta}{$\Delta$} |
|
15 \newcommand{\isasymTheta}{$\Theta$} |
|
16 \newcommand{\isasymLambda}{$\Lambda$} |
|
17 \newcommand{\isasymPi}{$\Pi$} |
|
18 \newcommand{\isasymSigma}{$\Sigma$} |
|
19 \newcommand{\isasymPhi}{$\Phi$} |
|
20 \newcommand{\isasymPsi}{$\Psi$} |
|
21 \newcommand{\isasymOmega}{$\Omega$} |
|
22 \newcommand{\isasymalpha}{$\alpha$} |
|
23 \newcommand{\isasymbeta}{$\beta$} |
|
24 \newcommand{\isasymgamma}{$\gamma$} |
|
25 \newcommand{\isasymdelta}{$\delta$} |
|
26 \newcommand{\isasymepsilon}{$\varepsilon$} |
|
27 \newcommand{\isasymzeta}{$\zeta$} |
|
28 \newcommand{\isasymeta}{$\eta$} |
|
29 \newcommand{\isasymtheta}{$\vartheta$} |
|
30 \newcommand{\isasymkappa}{$\kappa$} |
|
31 \newcommand{\isasymlambda}{$\lambda$} |
|
32 \newcommand{\isasymmu}{$\mu$} |
|
33 \newcommand{\isasymnu}{$\nu$} |
|
34 \newcommand{\isasymxi}{$\xi$} |
|
35 \newcommand{\isasympi}{$\pi$} |
|
36 \newcommand{\isasymrho}{$\rho$} |
|
37 \newcommand{\isasymsigma}{$\sigma$} |
|
38 \newcommand{\isasymtau}{$\tau$} |
|
39 \newcommand{\isasymphi}{$\varphi$} |
|
40 \newcommand{\isasymchi}{$\chi$} |
|
41 \newcommand{\isasympsi}{$\psi$} |
|
42 \newcommand{\isasymomega}{$\omega$} |
|
43 \newcommand{\isasymnot}{\emph{$\neg$}} |
|
44 \newcommand{\isasymand}{\emph{$\wedge$}} |
|
45 \newcommand{\isasymor}{\emph{$\vee$}} |
|
46 \newcommand{\isasymforall}{\emph{$\forall$}} |
|
47 \newcommand{\isasymexists}{\emph{$\exists$}} |
|
48 \newcommand{\isasymAnd}{\emph{$\bigwedge$}} |
|
49 \newcommand{\isasymlceil}{\emph{$\lceil$}} |
|
50 \newcommand{\isasymrceil}{\emph{$\rceil$}} |
|
51 \newcommand{\isasymlfloor}{\emph{$\lfloor$}} |
|
52 \newcommand{\isasymrfloor}{\emph{$\rfloor$}} |
|
53 \newcommand{\isasymturnstile}{\emph{$\vdash$}} |
|
54 \newcommand{\isasymTurnstile}{\emph{$\models$}} |
|
55 \newcommand{\isasymlbrakk}{\emph{$\mathopen{\lbrack\mkern-3mu\lbrack}$}} |
|
56 \newcommand{\isasymrbrakk}{\emph{$\mathclose{\rbrack\mkern-3mu\rbrack}$}} |
|
57 \newcommand{\isasymcdot}{\emph{$\cdot$}} |
|
58 \newcommand{\isasymin}{\emph{$\in$}} |
|
59 \newcommand{\isasymsubseteq}{\emph{$\subseteq$}} |
|
60 \newcommand{\isasyminter}{\emph{$\cap$}} |
|
61 \newcommand{\isasymunion}{\emph{$\cup$}} |
|
62 \newcommand{\isasymInter}{\emph{$\bigcap$}} |
|
63 \newcommand{\isasymUnion}{\emph{$\bigcup$}} |
|
64 \newcommand{\isasymsqinter}{\emph{$\sqcap$}} |
|
65 \newcommand{\isasymsqunion}{\emph{$\sqcup$}} |
|
66 \newcommand{\isasymSqinter}{\emph{$\bigsqcap$}} |
|
67 \newcommand{\isasymSqunion}{\emph{$\bigsqcup$}} |
|
68 \newcommand{\isasymbottom}{\emph{$\bot$}} |
|
69 \newcommand{\isasymdoteq}{\emph{$\doteq$}} |
|
70 \newcommand{\isasymequiv}{\emph{$\equiv$}} |
|
71 \newcommand{\isasymnoteq}{\emph{$\not=$}} |
|
72 \newcommand{\isasymsqsubset}{\emph{$\sqsubset$}} |
|
73 \newcommand{\isasymsqsubseteq}{\emph{$\sqsubseteq$}} |
|
74 \newcommand{\isasymprec}{\emph{$\prec$}} |
|
75 \newcommand{\isasympreceq}{\emph{$\preceq$}} |
|
76 \newcommand{\isasymsucc}{\emph{$\succ$}} |
|
77 \newcommand{\isasymapprox}{\emph{$\approx$}} |
|
78 \newcommand{\isasymsim}{\emph{$\sim$}} |
|
79 \newcommand{\isasymsimeq}{\emph{$\simeq$}} |
|
80 \newcommand{\isasymle}{\emph{$\le$}} |
|
81 \newcommand{\isasymColon}{\emph{$\mathrel{::}$}} |
|
82 \newcommand{\isasymleftarrow}{\emph{$\leftarrow$}} |
|
83 \newcommand{\isasymmidarrow}{\emph{$-$}}%deprecated |
|
84 \newcommand{\isasymrightarrow}{\emph{$\rightarrow$}} |
|
85 \newcommand{\isasymLeftarrow}{\emph{$\Leftarrow$}} |
|
86 \newcommand{\isasymMidarrow}{\emph{$=$}}%deprecated |
|
87 \newcommand{\isasymRightarrow}{\emph{$\Rightarrow$}} |
|
88 \newcommand{\isasymbow}{\emph{$\frown$}} |
|
89 \newcommand{\isasymmapsto}{\emph{$\mapsto$}} |
|
90 \newcommand{\isasymleadsto}{\emph{$\leadsto$}} |
|
91 \newcommand{\isasymup}{\emph{$\uparrow$}} |
|
92 \newcommand{\isasymdown}{\emph{$\downarrow$}} |
|
93 \newcommand{\isasymnotin}{\emph{$\notin$}} |
|
94 \newcommand{\isasymtimes}{\emph{$\times$}} |
|
95 \newcommand{\isasymoplus}{\emph{$\oplus$}} |
|
96 \newcommand{\isasymominus}{\emph{$\ominus$}} |
|
97 \newcommand{\isasymotimes}{\emph{$\otimes$}} |
|
98 \newcommand{\isasymoslash}{\emph{$\oslash$}} |
|
99 \newcommand{\isasymsubset}{\emph{$\subset$}} |
|
100 \newcommand{\isasyminfinity}{\emph{$\infty$}} |
|
101 \newcommand{\isasymbox}{\emph{$\Box$}} |
|
102 \newcommand{\isasymdiamond}{\emph{$\Diamond$}} |
|
103 \newcommand{\isasymcirc}{\emph{$\circ$}} |
|
104 \newcommand{\isasymbullet}{\emph{$\bullet$}} |
|
105 \newcommand{\isasymparallel}{\emph{$\parallel$}} |
|
106 \newcommand{\isasymsurd}{\emph{$\surd$}} |
|
107 \newcommand{\isasymcopyright}{\emph{\copyright}} |
|
108 |
|
109 \newcommand{\isasymplusminus}{\emph{$\pm$}} |
|
110 \newcommand{\isasymdiv}{\emph{$\div$}} |
|
111 \newcommand{\isasymlongrightarrow}{\emph{$\longrightarrow$}} |
|
112 \newcommand{\isasymlongleftarrow}{\emph{$\longleftarrow$}} |
|
113 \newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}} |
|
114 \newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}} |
|
115 \newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}} |
|
116 \newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}} |
|
117 %requires OT1 encoding: |
|
118 \newcommand{\isasymbrokenbar}{\emph{\textbrokenbar}} |
|
119 \newcommand{\isasymhyphen}{-} |
|
120 \newcommand{\isasymmacron}{\={}} |
|
121 \newcommand{\isasymexclamdown}{\emph{\textexclamdown}} |
|
122 \newcommand{\isasymquestiondown}{\emph{\textquestiondown}} |
|
123 %requires OT1 encoding: |
|
124 \newcommand{\isasymguillemotleft}{\emph{\guillemotleft}} |
|
125 %requires OT1 encoding: |
|
126 \newcommand{\isasymguillemotright}{\emph{\guillemotright}} |
|
127 %should be available (?): |
|
128 \newcommand{\isasymdegree}{\emph{\textdegree}} |
|
129 \newcommand{\isasymonesuperior}{\emph{$\mathonesuperior$}} |
|
130 \newcommand{\isasymonequarter}{\emph{\textonequarter}} |
|
131 \newcommand{\isasymtwosuperior}{\emph{$\mathtwosuperior$}} |
|
132 \newcommand{\isasymonehalf}{\emph{\textonehalf}} |
|
133 \newcommand{\isasymthreesuperior}{\emph{$\maththreesuperior$}} |
|
134 \newcommand{\isasymthreequarters}{\emph{\textthreequarters}} |
|
135 \newcommand{\isasymparagraph}{\emph{\P}} |
|
136 \newcommand{\isasymregistered}{\emph{\textregistered}} |
|
137 %should be available (?): |
|
138 \newcommand{\isasymordfeminine}{\emph{\textordfeminine}} |
|
139 %should be available (?): |
|
140 \newcommand{\isasymordmasculine}{\emph{\textordmasculine}} |
|
141 \newcommand{\isasymsection}{\S} |
|
142 \newcommand{\isasympounds}{\emph{$\pounds$}} |
|
143 %requires OT1 encoding: |
|
144 \newcommand{\isasymyen}{\emph{\textyen}} |
|
145 %requires OT1 encoding: |
|
146 \newcommand{\isasymcent}{\emph{\textcent}} |
|
147 %requires OT1 encoding: |
|
148 \newcommand{\isasymcurrency}{\emph{\textcurrency}} |