author | blanchet |
Mon, 15 Sep 2014 10:49:07 +0200 | |
changeset 58335 | a5a3b576fcfb |
parent 56451 | 856492b0f755 |
child 58618 | 782f0b662cae |
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 |
|
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 |
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} |
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 |
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
diff
changeset
|
41 |
end |