author | wenzelm |
Wed, 20 Jul 2016 21:26:11 +0200 | |
changeset 63531 | 847eefdca90d |
parent 61656 | cfabbc083977 |
child 67399 | eab6ce8368fa |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
2 |
||
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
3 |
theory Symbols |
63531 | 4 |
imports Main Base |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
5 |
begin |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
6 |
|
58618 | 7 |
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
|
8 |
|
58618 | 9 |
text \<open> |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
10 |
Isabelle supports an infinite number of non-ASCII symbols, which are |
61503 | 11 |
represented in source text as \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> (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
|
12 |
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
|
13 |
The collection of predefined standard symbols given below is |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
14 |
available by default for Isabelle document output, due to |
61503 | 15 |
appropriate definitions of \<^verbatim>\<open>\isasym\<close>\<open>name\<close> for each \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> in |
16 |
the \<^verbatim>\<open>isabellesym.sty\<close> 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 |
61503 | 20 |
\<^verbatim>\<open>\<^sup>\<close> for superscript and \<^verbatim>\<open>\<^sub>\<close> for subscript, |
21 |
such as \<^verbatim>\<open>A\<^sup>\<star>\<close> for \<open>A\<^sup>\<star>\<close> and \<^verbatim>\<open>A\<^sub>1\<close> for |
|
61493 | 22 |
\<open>A\<^sub>1\<close>. Sub- and superscripts that span a region of text can |
61503 | 23 |
be marked up with \<^verbatim>\<open>\<^bsub>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esub>\<close> and \<^verbatim>\<open>\<^bsup>\<close>\<open>\<dots>\<close>\<^verbatim>\<open>\<^esup>\<close> |
53060 | 24 |
respectively, but note that there are limitations in the typographic |
25 |
rendering quality of this form. Furthermore, all ASCII characters |
|
26 |
and most other symbols may be printed in bold by prefixing |
|
61503 | 27 |
\<^verbatim>\<open>\<^bold>\<close> such as \<^verbatim>\<open>\<^bold>\<alpha>\<close> for \<open>\<^bold>\<alpha>\<close>. Note that |
28 |
\<^verbatim>\<open>\<^sup>\<close>, \<^verbatim>\<open>\<^sub>\<close>, \<^verbatim>\<open>\<^bold>\<close> cannot be combined. |
|
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
29 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
30 |
Further details of Isabelle document preparation are covered in |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
31 |
\chref{ch:document-prep}. |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
32 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
33 |
\begin{center} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
34 |
\begin{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
35 |
\input{syms} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
36 |
\end{isabellebody} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
37 |
\end{center} |
58618 | 38 |
\<close> |
28838
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 |
end |