converted symbols.tex;
authorwenzelm
Mon Sep 15 20:51:58 2008 +0200 (2008-09-15 ago)
changeset 2822697c530dc8aca
parent 28225 5d1fc22bccdf
child 28227 77221ee0f7b9
converted symbols.tex;
doc-src/System/IsaMakefile
doc-src/System/Makefile
doc-src/System/Thy/ROOT.ML
doc-src/System/Thy/Symbols.thy
doc-src/System/Thy/document/Symbols.tex
doc-src/System/symbols.tex
doc-src/System/system.tex
     1.1 --- a/doc-src/System/IsaMakefile	Mon Sep 15 20:51:40 2008 +0200
     1.2 +++ b/doc-src/System/IsaMakefile	Mon Sep 15 20:51:58 2008 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4  
     1.5  Pure-System: $(LOG)/Pure-System.gz
     1.6  
     1.7 -$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML	\
     1.8 -  Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy
     1.9 +$(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
    1.10 +  Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy Thy/Symbols.thy
    1.11  	@$(USEDIR) -s System Pure Thy
    1.12  
    1.13  
     2.1 --- a/doc-src/System/Makefile	Mon Sep 15 20:51:40 2008 +0200
     2.2 +++ b/doc-src/System/Makefile	Mon Sep 15 20:51:58 2008 +0200
     2.3 @@ -12,10 +12,9 @@
     2.4  include ../Makefile.in
     2.5  
     2.6  NAME = system
     2.7 -FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \
     2.8 -	Thy/document/Presentation.tex symbols.tex ../iman.sty	 \
     2.9 -	../extra.sty ../ttbox.sty ../manual.bib			 \
    2.10 -
    2.11 +FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex	\
    2.12 +	Thy/document/Presentation.tex Thy/document/Symbols.tex		\
    2.13 +	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    2.14  OUTPUT = syms.tex
    2.15  
    2.16  syms.tex: showsymbols ../isabellesym.sty
     3.1 --- a/doc-src/System/Thy/ROOT.ML	Mon Sep 15 20:51:40 2008 +0200
     3.2 +++ b/doc-src/System/Thy/ROOT.ML	Mon Sep 15 20:51:58 2008 +0200
     3.3 @@ -7,3 +7,4 @@
     3.4  use_thy "Basics";
     3.5  use_thy "Presentation";
     3.6  use_thy "Misc";
     3.7 +use_thy "Symbols";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/System/Thy/Symbols.thy	Mon Sep 15 20:51:58 2008 +0200
     4.3 @@ -0,0 +1,49 @@
     4.4 +(* $Id$ *)
     4.5 +
     4.6 +theory Symbols
     4.7 +imports Pure
     4.8 +begin
     4.9 +
    4.10 +chapter {* Standard Isabelle symbols \label{app:symbols} *}
    4.11 +
    4.12 +text {*
    4.13 +  Isabelle supports an infinite number of non-ASCII symbols, which are
    4.14 +  represented in source text as @{verbatim "\\"}@{verbatim "<"}@{text
    4.15 +  name}@{verbatim ">"} (where @{text name} may be any identifier).  It
    4.16 +  is left to front-end tools how to present these symbols to the user.
    4.17 +  The collection of predefined standard symbols given below is
    4.18 +  available by default for Isabelle document output, due to
    4.19 +  appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
    4.20 +  name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
    4.21 +  ">"} in the @{verbatim isabellesym.sty} file.  Most of these symbols
    4.22 +  are displayed properly in Proof~General if used with the X-Symbol
    4.23 +  package.
    4.24 +
    4.25 +  Moreover, any single symbol (or ASCII character) may be prefixed by
    4.26 +  @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
    4.27 +  "\\"}@{verbatim "<^sub>"}, for subscript, such as @{verbatim
    4.28 +  "A\\"}@{verbatim "<^sup>\<star>"}, for @{text "A\<^sup>\<star>"} the alternative
    4.29 +  versions @{verbatim "\\"}@{verbatim "<^isub>"} and @{verbatim
    4.30 +  "\\"}@{verbatim "<^isup>"} are considered as quasi letters and may
    4.31 +  be used within identifiers.  Sub- and superscripts that span a
    4.32 +  region of text are marked up with @{verbatim "\\"}@{verbatim
    4.33 +  "<^bsub>"}@{text "\<dots>"}@{verbatim "\\"}@{verbatim "<^esub>"}, and
    4.34 +  @{verbatim "\\"}@{verbatim "<^bsup>"}@{text "\<dots>"}@{verbatim
    4.35 +  "\\"}@{verbatim "<^esup>"} respectively.  Furthermore, all ASCII
    4.36 +  characters and most other symbols may be printed in bold by
    4.37 +  prefixing @{verbatim "\\"}@{verbatim "<^bold>"} such as @{verbatim
    4.38 +  "\\"}@{verbatim "<^bold>\\"}@{verbatim "<alpha>"} for @{text
    4.39 +  "\<^bold>\<alpha>"}.  Note that @{verbatim "\\"}@{verbatim "<^bold>"}, may
    4.40 +  \emph{not} be combined with sub- or superscripts for single symbols.
    4.41 +
    4.42 +  Further details of Isabelle document preparation are covered in
    4.43 +  \chref{ch:present}.
    4.44 +
    4.45 +  \begin{center}
    4.46 +  \begin{isabellebody}
    4.47 +  \input{syms}  
    4.48 +  \end{isabellebody}
    4.49 +  \end{center}
    4.50 +*}
    4.51 +
    4.52 +end
    4.53 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/System/Thy/document/Symbols.tex	Mon Sep 15 20:51:58 2008 +0200
     5.3 @@ -0,0 +1,75 @@
     5.4 +%
     5.5 +\begin{isabellebody}%
     5.6 +\def\isabellecontext{Symbols}%
     5.7 +%
     5.8 +\isadelimtheory
     5.9 +\isanewline
    5.10 +\isanewline
    5.11 +%
    5.12 +\endisadelimtheory
    5.13 +%
    5.14 +\isatagtheory
    5.15 +\isacommand{theory}\isamarkupfalse%
    5.16 +\ Symbols\isanewline
    5.17 +\isakeyword{imports}\ Pure\isanewline
    5.18 +\isakeyword{begin}%
    5.19 +\endisatagtheory
    5.20 +{\isafoldtheory}%
    5.21 +%
    5.22 +\isadelimtheory
    5.23 +%
    5.24 +\endisadelimtheory
    5.25 +%
    5.26 +\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
    5.27 +}
    5.28 +\isamarkuptrue%
    5.29 +%
    5.30 +\begin{isamarkuptext}%
    5.31 +Isabelle supports an infinite number of non-ASCII symbols, which are
    5.32 +  represented in source text as \verb|\|\verb|<|\isa{name}\verb|>| (where \isa{name} may be any identifier).  It
    5.33 +  is left to front-end tools how to present these symbols to the user.
    5.34 +  The collection of predefined standard symbols given below is
    5.35 +  available by default for Isabelle document output, due to
    5.36 +  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
    5.37 +  are displayed properly in Proof~General if used with the X-Symbol
    5.38 +  package.
    5.39 +
    5.40 +  Moreover, any single symbol (or ASCII character) may be prefixed by
    5.41 +  \verb|\|\verb|<^sup>|, for superscript and \verb|\|\verb|<^sub>|, for subscript, such as \verb|A\|\verb|<^sup>\<star>|, for \isa{{\isachardoublequote}A\isactrlsup {\isasymstar}{\isachardoublequote}} the alternative
    5.42 +  versions \verb|\|\verb|<^isub>| and \verb|\|\verb|<^isup>| are considered as quasi letters and may
    5.43 +  be used within identifiers.  Sub- and superscripts that span a
    5.44 +  region of text are marked up with \verb|\|\verb|<^bsub>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esub>|, and
    5.45 +  \verb|\|\verb|<^bsup>|\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}\verb|\|\verb|<^esup>| respectively.  Furthermore, all ASCII
    5.46 +  characters and most other symbols may be printed in bold by
    5.47 +  prefixing \verb|\|\verb|<^bold>| such as \verb|\|\verb|<^bold>\|\verb|<alpha>| for \isa{{\isachardoublequote}\isactrlbold {\isasymalpha}{\isachardoublequote}}.  Note that \verb|\|\verb|<^bold>|, may
    5.48 +  \emph{not} be combined with sub- or superscripts for single symbols.
    5.49 +
    5.50 +  Further details of Isabelle document preparation are covered in
    5.51 +  \chref{ch:present}.
    5.52 +
    5.53 +  \begin{center}
    5.54 +  \begin{isabellebody}
    5.55 +  \input{syms}  
    5.56 +  \end{isabellebody}
    5.57 +  \end{center}%
    5.58 +\end{isamarkuptext}%
    5.59 +\isamarkuptrue%
    5.60 +%
    5.61 +\isadelimtheory
    5.62 +%
    5.63 +\endisadelimtheory
    5.64 +%
    5.65 +\isatagtheory
    5.66 +\isacommand{end}\isamarkupfalse%
    5.67 +%
    5.68 +\endisatagtheory
    5.69 +{\isafoldtheory}%
    5.70 +%
    5.71 +\isadelimtheory
    5.72 +%
    5.73 +\endisadelimtheory
    5.74 +\end{isabellebody}%
    5.75 +%%% Local Variables:
    5.76 +%%% mode: latex
    5.77 +%%% TeX-master: "root"
    5.78 +%%% End:
     6.1 --- a/doc-src/System/symbols.tex	Mon Sep 15 20:51:40 2008 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,39 +0,0 @@
     6.4 -
     6.5 -% $Id$
     6.6 -
     6.7 -\chapter{Standard Isabelle symbols}\label{app:symbols}
     6.8 -
     6.9 -Isabelle supports an infinite number of non-ASCII symbols, which are
    6.10 -represented in source text as \verb,\<,$name$\verb,>, (where $name$ may be any
    6.11 -identifier).  It is left to front-end tools how to present these symbols to
    6.12 -the user.  The collection of predefined standard symbols given below is
    6.13 -available by default for Isabelle document output, due to appropriate
    6.14 -definitions of \verb,\isasym,$name$ for each \verb,\<,$name$\verb,>, in the
    6.15 -\verb,isabellesym.sty, file.  Most of these symbols are displayed properly in
    6.16 -Proof~General if used with the X-Symbol package.
    6.17 -
    6.18 -Moreover, any single symbol (or ASCII character) may be prefixed by
    6.19 -\verb,\<^sup>, for superscript and \verb,\<^sub>, for subscript, such as
    6.20 -\verb,A\<^sup>\<star>, for \isa{A\isactrlsup{\isasymstar}}; the alternative
    6.21 -versions \verb,\<^isub>, and \verb,\<^isup>, are considered as quasi letters
    6.22 -and may be used within identifiers.  Sub- and superscripts that span a region
    6.23 -of text are marked up with \verb,\<^bsub>,\dots\verb,\<^esub>, and
    6.24 -\verb,\<^bsup>,\dots\verb,\<^esup>,, respectively.  Furthermore, all ASCII
    6.25 -characters and most other symbols may be printed in bold by prefixing
    6.26 -\verb,\<^bold>,, such as \verb,\<^bold>\<alpha>, for
    6.27 -\isa{\isactrlbold{\isasymalpha}}.  Note that \verb,\<^bold>, may \emph{not} be
    6.28 -combined with sub- or superscripts for single symbols.
    6.29 -
    6.30 -Further details of Isabelle document preparation are covered in
    6.31 -chapter~\ref{ch:present}.
    6.32 -
    6.33 -\begin{center}
    6.34 -  \begin{isabellebody}
    6.35 -    \input{syms}  
    6.36 -  \end{isabellebody}
    6.37 -\end{center}
    6.38 -
    6.39 -%%% Local Variables: 
    6.40 -%%% mode: latex
    6.41 -%%% TeX-master: "system"
    6.42 -%%% End: 
     7.1 --- a/doc-src/System/system.tex	Mon Sep 15 20:51:40 2008 +0200
     7.2 +++ b/doc-src/System/system.tex	Mon Sep 15 20:51:58 2008 +0200
     7.3 @@ -42,7 +42,7 @@
     7.4  
     7.5  \appendix
     7.6  \let\int\intorig
     7.7 -\input{symbols}
     7.8 +\input{Thy/document/Symbols}
     7.9  
    7.10  \begingroup
    7.11    \bibliographystyle{plain} \small\raggedright\frenchspacing