author | wenzelm |
Wed, 15 Apr 2009 11:14:48 +0200 | |
changeset 30895 | bad26d8f0adf |
parent 30242 | aea5d7fa7ef5 |
child 42651 | e3fdb7c96be5 |
permissions | -rw-r--r-- |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
1 |
theory Symbols |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
2 |
imports Pure |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
3 |
begin |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
4 |
|
29719 | 5 |
chapter {* Predefined Isabelle symbols \label{app:symbols} *} |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
6 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
7 |
text {* |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
8 |
Isabelle supports an infinite number of non-ASCII symbols, which are |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
9 |
represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
10 |
name}@{verbatim ">"} (where @{text name} may be any identifier). It |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
11 |
is left to front-end tools how to present these symbols to the user. |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
12 |
The collection of predefined standard symbols given below is |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
13 |
available by default for Isabelle document output, due to |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
14 |
appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
15 |
name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
16 |
">"} in the @{verbatim isabellesym.sty} file. Most of these symbols |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
17 |
are displayed properly in Proof~General if used with the X-Symbol |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
18 |
package. |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
19 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
20 |
Moreover, any single symbol (or ASCII character) may be prefixed by |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
21 |
@{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
22 |
"\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
23 |
"A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
24 |
versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
25 |
"\\"}@{verbatim "<^isup>"} are considered as quasi letters and may |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
26 |
be used within identifiers. Sub- and superscripts that span a |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
27 |
region of text are marked up with @{verbatim "\\"}@{verbatim |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
28 |
"<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
29 |
@{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
30 |
"\\"}@{verbatim "<^esup>"} respectively. Furthermore, all ASCII |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
31 |
characters and most other symbols may be printed in bold by |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
32 |
prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
33 |
"\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
34 |
"\<^bold>\<alpha>"}. Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
35 |
\emph{not} be combined with sub- or superscripts for single symbols. |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
36 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
37 |
Further details of Isabelle document preparation are covered in |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
38 |
\chref{ch:document-prep}. |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
39 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
40 |
\begin{center} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
41 |
\begin{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
42 |
\input{syms} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
43 |
\end{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
44 |
\end{center} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
45 |
*} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
46 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
47 |
end |