author | wenzelm |
Tue, 20 Oct 2015 23:53:40 +0200 | |
changeset 61493 | 0debd22f0c0e |
parent 58724 | e5f809f52f26 |
child 61503 | 28e788ca2c5d |
permissions | -rw-r--r-- |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
1 |
theory Symbols |
42651 | 2 |
imports Base Main |
28838
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 |
|
58618 | 5 |
chapter \<open>Predefined Isabelle symbols \label{app:symbols}\<close> |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
6 |
|
58618 | 7 |
text \<open> |
28838
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 |
61493 | 9 |
represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}\<open>name\<close>@{verbatim ">"} (where \<open>name\<close> may be any identifier). It |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
10 |
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
|
11 |
The collection of predefined standard symbols given below is |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
12 |
available by default for Isabelle document output, due to |
61493 | 13 |
appropriate definitions of @{verbatim \<open>\isasym\<close>}\<open>name\<close> for each @{verbatim \<open>\\<close>}@{verbatim "<"}\<open>name\<close>@{verbatim |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
14 |
">"} in the @{verbatim isabellesym.sty} file. Most of these symbols |
53060 | 15 |
are displayed properly in Isabelle/jEdit and {\LaTeX} generated from Isabelle. |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
16 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
17 |
Moreover, any single symbol (or ASCII character) may be prefixed by |
53060 | 18 |
@{verbatim "\<^sup>"} for superscript and @{verbatim "\<^sub>"} for subscript, |
61493 | 19 |
such as @{verbatim "A\<^sup>\<star>"} for \<open>A\<^sup>\<star>\<close> and @{verbatim "A\<^sub>1"} for |
20 |
\<open>A\<^sub>1\<close>. Sub- and superscripts that span a region of text can |
|
21 |
be marked up with @{verbatim "\<^bsub>"}\<open>\<dots>\<close>@{verbatim |
|
22 |
"\<^esub>"} and @{verbatim "\<^bsup>"}\<open>\<dots>\<close>@{verbatim "\<^esup>"} |
|
53060 | 23 |
respectively, but note that there are limitations in the typographic |
24 |
rendering quality of this form. Furthermore, all ASCII characters |
|
25 |
and most other symbols may be printed in bold by prefixing |
|
61493 | 26 |
@{verbatim "\<^bold>"} such as @{verbatim "\<^bold>\<alpha>"} for \<open>\<^bold>\<alpha>\<close>. Note that |
53060 | 27 |
@{verbatim "\<^sup>"}, @{verbatim "\<^sub>"}, @{verbatim "\<^bold>"} cannot be combined. |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
28 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
29 |
Further details of Isabelle document preparation are covered in |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
30 |
\chref{ch:document-prep}. |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
31 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
32 |
\begin{center} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
33 |
\begin{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
34 |
\input{syms} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
35 |
\end{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
36 |
\end{center} |
58618 | 37 |
\<close> |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
38 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
39 |
end |