equal
deleted
inserted
replaced
1 theory Symbols |
1 theory Symbols |
2 imports Base Main |
2 imports Base Main |
3 begin |
3 begin |
4 |
4 |
5 chapter {* Predefined Isabelle symbols \label{app:symbols} *} |
5 chapter \<open>Predefined Isabelle symbols \label{app:symbols}\<close> |
6 |
6 |
7 text {* |
7 text \<open> |
8 Isabelle supports an infinite number of non-ASCII symbols, which are |
8 Isabelle supports an infinite number of non-ASCII symbols, which are |
9 represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text |
9 represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text |
10 name}@{verbatim ">"} (where @{text name} may be any identifier). It |
10 name}@{verbatim ">"} (where @{text name} may be any identifier). It |
11 is left to front-end tools how to present these symbols to the user. |
11 is left to front-end tools how to present these symbols to the user. |
12 The collection of predefined standard symbols given below is |
12 The collection of predefined standard symbols given below is |
34 \begin{center} |
34 \begin{center} |
35 \begin{isabellebody} |
35 \begin{isabellebody} |
36 \input{syms} |
36 \input{syms} |
37 \end{isabellebody} |
37 \end{isabellebody} |
38 \end{center} |
38 \end{center} |
39 *} |
39 \<close> |
40 |
40 |
41 end |
41 end |