author | wenzelm |
Sun, 30 Nov 2014 14:02:48 +0100 | |
changeset 59067 | dd8ec9138112 |
parent 58724 | e5f809f52f26 |
child 61493 | 0debd22f0c0e |
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 |
58724 | 9 |
represented in source text as @{verbatim \<open>\\<close>}@{verbatim "<"}@{text |
28838
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 |
58724 | 14 |
appropriate definitions of @{verbatim \<open>\isasym\<close>}@{text |
15 |
name} for each @{verbatim \<open>\\<close>}@{verbatim "<"}@{text name}@{verbatim |
|
28838
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 |
53060 | 17 |
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
|
18 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
19 |
Moreover, any single symbol (or ASCII character) may be prefixed by |
53060 | 20 |
@{verbatim "\<^sup>"} for superscript and @{verbatim "\<^sub>"} for subscript, |
21 |
such as @{verbatim "A\<^sup>\<star>"} for @{text "A\<^sup>\<star>"} and @{verbatim "A\<^sub>1"} for |
|
22 |
@{text "A\<^sub>1"}. Sub- and superscripts that span a region of text can |
|
23 |
be marked up with @{verbatim "\<^bsub>"}@{text "\<dots>"}@{verbatim |
|
24 |
"\<^esub>"} and @{verbatim "\<^bsup>"}@{text "\<dots>"}@{verbatim "\<^esup>"} |
|
25 |
respectively, but note that there are limitations in the typographic |
|
26 |
rendering quality of this form. Furthermore, all ASCII characters |
|
27 |
and most other symbols may be printed in bold by prefixing |
|
28 |
@{verbatim "\<^bold>"} such as @{verbatim "\<^bold>\<alpha>"} for @{text "\<^bold>\<alpha>"}. Note that |
|
29 |
@{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
|
30 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
31 |
Further details of Isabelle document preparation are covered in |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
32 |
\chref{ch:document-prep}. |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
33 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
34 |
\begin{center} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
35 |
\begin{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
36 |
\input{syms} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
37 |
\end{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
38 |
\end{center} |
58618 | 39 |
\<close> |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
40 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
41 |
end |