equal
deleted
inserted
replaced
4 %% License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 %% License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 %% |
5 %% |
6 %% definitions of standard Isabelle symbols |
6 %% definitions of standard Isabelle symbols |
7 %% |
7 %% |
8 |
8 |
9 % required packages for unusual symbols -- see below for details |
9 % Required packages for unusual symbols -- see below for details. |
10 %\usepackage{latexsym} |
10 %\usepackage{latexsym} |
11 %\usepackage{amssymb} |
11 %\usepackage{amssymb} |
12 %\usepackage[english]{babel} |
12 %\usepackage[english]{babel} |
13 %\usepackage[latin1]{inputenc} |
13 %\usepackage[latin1]{inputenc} |
14 %\usepackage[only,bigsqcap]{stmaryrd} |
14 %\usepackage[only,bigsqcap]{stmaryrd} |
15 %\usepackage{wasysym} |
15 %\usepackage{wasysym} |
16 |
16 |
17 % Note: \emph is the key to proper spacing in fake math mode; it |
17 % Note: \emph is important for proper spacing in fake math mode, it |
18 % automatically inserts italic corrections around symbols wherever |
18 % automatically inserts italic corrections around symbols wherever |
19 % appropriate. |
19 % appropriate. |
20 |
20 |
21 \newcommand{\isasymspacespace}{~~} |
21 \newcommand{\isasymspacespace}{~~} |
22 \newcommand{\isasymGamma}{$\Gamma$} |
22 \newcommand{\isasymGamma}{$\Gamma$} |
125 \newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}} |
125 \newcommand{\isasymlongleftrightarrow}{\emph{$\longleftrightarrow$}} |
126 \newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}} |
126 \newcommand{\isasymLongrightarrow}{\emph{$\Longrightarrow$}} |
127 \newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}} |
127 \newcommand{\isasymLongleftarrow}{\emph{$\Longleftarrow$}} |
128 \newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}} |
128 \newcommand{\isasymLongleftrightarrow}{\emph{$\Longleftrightarrow$}} |
129 \newcommand{\isasymbar}{\emph{$\mid$}} |
129 \newcommand{\isasymbar}{\emph{$\mid$}} |
130 \newcommand{\isasymhyphen}{-} |
130 \newcommand{\isasymhyphen}{\emph{\rm-}} |
131 \newcommand{\isasymmacron}{\={}} |
131 \newcommand{\isasymmacron}{\emph{\rm\=\relax}} |
132 \newcommand{\isasymexclamdown}{\emph{\rm\textexclamdown}} |
132 \newcommand{\isasymexclamdown}{\emph{\rm\textexclamdown}} |
133 \newcommand{\isasymquestiondown}{\emph{\rm\textquestiondown}} |
133 \newcommand{\isasymquestiondown}{\emph{\rm\textquestiondown}} |
134 \newcommand{\isasymguillemotleft}{\emph{\flqq}} %requires babel |
134 \newcommand{\isasymguillemotleft}{\emph{\flqq}} %requires babel |
135 \newcommand{\isasymguillemotright}{\emph{\frqq}} %requires babel |
135 \newcommand{\isasymguillemotright}{\emph{\frqq}} %requires babel |
136 \newcommand{\isasymdegree}{\emph{\rm\textdegree}} %requires latin1 |
136 \newcommand{\isasymdegree}{\emph{\rm\textdegree}} %requires latin1 |
142 \newcommand{\isasymthreequarters}{\emph{\rm\textthreequarters}} %requires latin1 |
142 \newcommand{\isasymthreequarters}{\emph{\rm\textthreequarters}} %requires latin1 |
143 \newcommand{\isasymparagraph}{\emph{\P}} |
143 \newcommand{\isasymparagraph}{\emph{\P}} |
144 \newcommand{\isasymregistered}{\emph{\rm\textregistered}} |
144 \newcommand{\isasymregistered}{\emph{\rm\textregistered}} |
145 \newcommand{\isasymordfeminine}{\emph{\rm\textordfeminine}} |
145 \newcommand{\isasymordfeminine}{\emph{\rm\textordfeminine}} |
146 \newcommand{\isasymordmasculine}{\emph{\rm\textordmasculine}} |
146 \newcommand{\isasymordmasculine}{\emph{\rm\textordmasculine}} |
147 \newcommand{\isasymsection}{\S} |
147 \newcommand{\isasymsection}{\emph{\S}} |
148 \newcommand{\isasympounds}{\emph{$\pounds$}} |
148 \newcommand{\isasympounds}{\emph{$\pounds$}} |
149 \newcommand{\isasymyen}{\emph{\yen}} %requires amssymb |
149 \newcommand{\isasymyen}{\emph{\yen}} %requires amssymb |
150 \newcommand{\isasymcent}{\emph{\cent}} %requires wasysym |
150 \newcommand{\isasymcent}{\emph{\cent}} %requires wasysym |
151 \newcommand{\isasymcurrency}{\emph{\currency}} %requires wasysym |
151 \newcommand{\isasymcurrency}{\emph{\currency}} %requires wasysym |
152 \newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}} |
152 \newcommand{\isasymlbrace}{\emph{$\mathopen{\lbrace\mkern-4.5mu\mid}$}} |
230 \newcommand{\isasymlesssim}{\emph{$\lesssim$}} %requires amssymb |
230 \newcommand{\isasymlesssim}{\emph{$\lesssim$}} %requires amssymb |
231 \newcommand{\isasymgreatersim}{\emph{$\gtrsim$}} %requires amssymb |
231 \newcommand{\isasymgreatersim}{\emph{$\gtrsim$}} %requires amssymb |
232 \newcommand{\isasymlessapprox}{\emph{$\lessapprox$}} %requires amssymb |
232 \newcommand{\isasymlessapprox}{\emph{$\lessapprox$}} %requires amssymb |
233 \newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}} %requires amssymb |
233 \newcommand{\isasymgreaterapprox}{\emph{$\gtrapprox$}} %requires amssymb |
234 \newcommand{\isasymtriangleq}{\emph{$\triangleq$}} %requires amssymb |
234 \newcommand{\isasymtriangleq}{\emph{$\triangleq$}} %requires amssymb |
|
235 \newcommand{\isasymlparr}{\emph{$\mathopen{(\mkern-3mu\mid}$}} |
|
236 \newcommand{\isasymrparr}{\emph{$\mathclose{\mid\mkern-3mu)}$}} |