# HG changeset patch # User wenzelm # Date 1221504718 -7200 # Node ID 97c530dc8aca9d4897b9fec302511859fa52fd1b # Parent 5d1fc22bccdf6925372ddbdf610ae64be98a1df2 converted symbols.tex; diff -r 5d1fc22bccdf -r 97c530dc8aca doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Mon Sep 15 20:51:40 2008 +0200 +++ b/doc-src/System/IsaMakefile Mon Sep 15 20:51:58 2008 +0200 @@ -21,8 +21,8 @@ Pure-System: $(LOG)/Pure-System.gz -$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy +$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \ + Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy Thy/Symbols.thy @$(USEDIR) -s System Pure Thy diff -r 5d1fc22bccdf -r 97c530dc8aca doc-src/System/Makefile --- a/doc-src/System/Makefile Mon Sep 15 20:51:40 2008 +0200 +++ b/doc-src/System/Makefile Mon Sep 15 20:51:58 2008 +0200 @@ -12,10 +12,9 @@ include ../Makefile.in NAME = system -FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \ - Thy/document/Presentation.tex symbols.tex ../iman.sty \ - ../extra.sty ../ttbox.sty ../manual.bib \ - +FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \ + Thy/document/Presentation.tex Thy/document/Symbols.tex \ + ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib OUTPUT = syms.tex syms.tex: showsymbols ../isabellesym.sty diff -r 5d1fc22bccdf -r 97c530dc8aca doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Mon Sep 15 20:51:40 2008 +0200 +++ b/doc-src/System/Thy/ROOT.ML Mon Sep 15 20:51:58 2008 +0200 @@ -7,3 +7,4 @@ use_thy "Basics"; use_thy "Presentation"; use_thy "Misc"; +use_thy "Symbols"; diff -r 5d1fc22bccdf -r 97c530dc8aca doc-src/System/Thy/Symbols.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Symbols.thy Mon Sep 15 20:51:58 2008 +0200 @@ -0,0 +1,49 @@ +(* $Id$ *) + +theory Symbols +imports Pure +begin + +chapter {* Standard Isabelle symbols \label{app:symbols} *} + +text {* + Isabelle supports an infinite number of non-ASCII symbols, which are + represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text + name}@{verbatim ">"} (where @{text name} may be any identifier). It + is left to front-end tools how to present these symbols to the user. + The collection of predefined standard symbols given below is + available by default for Isabelle document output, due to + appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text + name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim + ">"} in the @{verbatim isabellesym.sty} file. Most of these symbols + are displayed properly in Proof~General if used with the X-Symbol + package. + + Moreover, any single symbol (or ASCII character) may be prefixed by + @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim + "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim + "A\\"}@{verbatim "<^sup>\"}, for @{text "A\<^sup>\"} the alternative + versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim + "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may + be used within identifiers. Sub- and superscripts that span a + region of text are marked up with @{verbatim "\\"}@{verbatim + "<^bsub>"}@{text "\"}@{verbatim "\\"}@{verbatim "<^esub>"}, and + @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\"}@{verbatim + "\\"}@{verbatim "<^esup>"} respectively. Furthermore, all ASCII + characters and most other symbols may be printed in bold by + prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim + "\\"}@{verbatim "<^bold>\\"}@{verbatim ""} for @{text + "\<^bold>\"}. Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may + \emph{not} be combined with sub- or superscripts for single symbols. + + Further details of Isabelle document preparation are covered in + \chref{ch:present}. + + \begin{center} + \begin{isabellebody} + \input{syms} + \end{isabellebody} + \end{center} +*} + +end \ No newline at end of file diff -r 5d1fc22bccdf -r 97c530dc8aca doc-src/System/Thy/document/Symbols.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/document/Symbols.tex Mon Sep 15 20:51:58 2008 +0200 @@ -0,0 +1,75 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Symbols}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Symbols\isanewline +\isakeyword{imports}\ Pure\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isabelle supports an infinite number of non-ASCII symbols, which are + represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier). It + is left to front-end tools how to present these symbols to the user. + The collection of predefined standard symbols given below is + available by default for Isabelle document output, due to + appropriate definitions of \verb|\|\verb|isasym|\isa{name} for each \verb|\|\verb|<|\isa{name}\verb|>| in the \verb|isabellesym.sty| file. Most of these symbols + are displayed properly in Proof~General if used with the X-Symbol + package. + + Moreover, any single symbol (or ASCII character) may be prefixed by + \verb|\|\verb|<^sup>|, for superscript and \verb|\|\verb|<^sub>|, for subscript, such as \verb|A\|\verb|<^sup>\|, for \isa{{\isachardoublequote}A\isactrlsup {\isasymstar}{\isachardoublequote}} the alternative + versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may + be used within identifiers. Sub- and superscripts that span a + region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and + \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively. Furthermore, all ASCII + characters and most other symbols may be printed in bold by + prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}. Note that \verb|\|\verb|<^bold>|, may + \emph{not} be combined with sub- or superscripts for single symbols. + + Further details of Isabelle document preparation are covered in + \chref{ch:present}. + + \begin{center} + \begin{isabellebody} + \input{syms} + \end{isabellebody} + \end{center}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 5d1fc22bccdf -r 97c530dc8aca doc-src/System/symbols.tex --- a/doc-src/System/symbols.tex Mon Sep 15 20:51:40 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ - -% $Id$ - -\chapter{Standard Isabelle symbols}\label{app:symbols} - -Isabelle supports an infinite number of non-ASCII symbols, which are -represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any -identifier). It is left to front-end tools how to present these symbols to -the user. The collection of predefined standard symbols given below is -available by default for Isabelle document output, due to appropriate -definitions of \verb,\isasym,$name$ for each \verb,\<,$name$\verb,>, in the -\verb,isabellesym.sty, file. Most of these symbols are displayed properly in -Proof~General if used with the X-Symbol package. - -Moreover, any single symbol (or ASCII character) may be prefixed by -\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as -\verb,A\<^sup>\, for \isa{A\isactrlsup{\isasymstar}}; the alternative -versions \verb,\<^isub>, and \verb,\<^isup>, are considered as quasi letters -and may be used within identifiers. Sub- and superscripts that span a region -of text are marked up with \verb,\<^bsub>,\dots\verb,\<^esub>, and -\verb,\<^bsup>,\dots\verb,\<^esup>,, respectively. Furthermore, all ASCII -characters and most other symbols may be printed in bold by prefixing -\verb,\<^bold>,, such as \verb,\<^bold>\, for -\isa{\isactrlbold{\isasymalpha}}. Note that \verb,\<^bold>, may \emph{not} be -combined with sub- or superscripts for single symbols. - -Further details of Isabelle document preparation are covered in -chapter~\ref{ch:present}. - -\begin{center} - \begin{isabellebody} - \input{syms} - \end{isabellebody} -\end{center} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "system" -%%% End: diff -r 5d1fc22bccdf -r 97c530dc8aca doc-src/System/system.tex --- a/doc-src/System/system.tex Mon Sep 15 20:51:40 2008 +0200 +++ b/doc-src/System/system.tex Mon Sep 15 20:51:58 2008 +0200 @@ -42,7 +42,7 @@ \appendix \let\int\intorig -\input{symbols} +\input{Thy/document/Symbols} \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing