# HG changeset patch # User wenzelm # Date 1227029110 -3600 # Node ID d5db6dfcb34a0fd26f8d3c4b161f64ef81dbe22c # Parent c6b17889237a5aaacd63f378548ea96f1cb6d826 moved table of standard Isabelle symbols to isar-ref manual; diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/IsaMakefile --- a/doc-src/IsarRef/IsaMakefile Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/IsaMakefile Tue Nov 18 18:25:10 2008 +0100 @@ -25,7 +25,7 @@ Thy/Inner_Syntax.thy Thy/Introduction.thy Thy/Outer_Syntax.thy \ Thy/Spec.thy Thy/Proof.thy Thy/Misc.thy Thy/Document_Preparation.thy \ Thy/Generic.thy Thy/HOL_Specific.thy Thy/Quick_Reference.thy \ - Thy/ML_Tactic.thy + Thy/Symbols.thy Thy/ML_Tactic.thy @$(USEDIR) -s IsarRef HOL Thy diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/Makefile Tue Nov 18 18:25:10 2008 +0100 @@ -19,14 +19,20 @@ Thy/document/Quick_Reference.tex Thy/document/Spec.tex \ Thy/document/ZF_Specific.tex Thy/document/Inner_Syntax.tex \ Thy/document/Introduction.tex Thy/document/Document_Preparation.tex \ - Thy/document/Misc.tex Thy/document/Outer_Syntax.tex ../isar.sty \ - ../rail.sty ../railsetup.sty ../proof.sty ../iman.sty ../extra.sty \ - ../ttbox.sty ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \ - ../manual.bib + Thy/document/Misc.tex Thy/document/Outer_Syntax.tex \ + Thy/document/Symbols.tex ../isar.sty ../rail.sty ../railsetup.sty \ + ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../isabelle.sty \ + ../isabellesym.sty ../pdfsetup.sty ../manual.bib + +OUTPUT = syms.tex + +syms.tex: showsymbols ../isabellesym.sty + @./showsymbols <../isabellesym.sty >syms.tex + dvi: $(NAME).dvi -$(NAME).dvi: $(FILES) isabelle_isar.eps +$(NAME).dvi: $(FILES) isabelle_isar.eps syms.tex $(LATEX) $(NAME) $(RAIL) $(NAME) $(BIBTEX) $(NAME) @@ -37,7 +43,7 @@ pdf: $(NAME).pdf -$(NAME).pdf: $(FILES) isabelle_isar.pdf +$(NAME).pdf: $(FILES) isabelle_isar.pdf syms.tex $(PDFLATEX) $(NAME) $(RAIL) $(NAME) $(BIBTEX) $(NAME) diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Thy/Outer_Syntax.thy --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Tue Nov 18 18:25:10 2008 +0100 @@ -171,9 +171,9 @@ symbols like this, although proper presentation is left to front-end tools such as {\LaTeX} or Proof~General with the X-Symbol package. A list of standard Isabelle symbols that work well with these tools - is given in \cite[appendix~A]{isabelle-sys}. Note that @{verbatim - "\"} does not belong to the @{text letter} category, since it is - already used differently in the Pure term language. + is given in \appref{app:symbols}. Note that @{verbatim "\"} does + not belong to the @{text letter} category, since it is already used + differently in the Pure term language. *} diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/Thy/Proof.thy Tue Nov 18 18:25:10 2008 +0100 @@ -105,7 +105,7 @@ A typical application of @{command "oops"} is to explain Isar proofs \emph{within} the system itself, in conjunction with the document - preparation tools of Isabelle described in \cite{isabelle-sys}. + preparation tools of Isabelle described in \chref{ch:document-prep}. Thus partial or even wrong proof attempts can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} macros can be easily adapted to print something like ``@{text "\"}'' instead of diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Thy/ROOT.ML --- a/doc-src/IsarRef/Thy/ROOT.ML Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/Thy/ROOT.ML Tue Nov 18 18:25:10 2008 +0100 @@ -14,4 +14,5 @@ use_thy "Generic"; use_thy "HOL_Specific"; use_thy "Quick_Reference"; +use_thy "Symbols"; use_thy "ML_Tactic"; diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Thy/Symbols.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/Symbols.thy Tue Nov 18 18:25:10 2008 +0100 @@ -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:document-prep}. + + \begin{center} + \begin{isabellebody} + \input{syms} + \end{isabellebody} + \end{center} +*} + +end \ No newline at end of file diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Thy/document/Outer_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Tue Nov 18 18:25:10 2008 +0100 @@ -186,8 +186,9 @@ symbols like this, although proper presentation is left to front-end tools such as {\LaTeX} or Proof~General with the X-Symbol package. A list of standard Isabelle symbols that work well with these tools - is given in \cite[appendix~A]{isabelle-sys}. Note that \verb|\| does not belong to the \isa{letter} category, since it is - already used differently in the Pure term language.% + is given in \appref{app:symbols}. Note that \verb|\| does + not belong to the \isa{letter} category, since it is already used + differently in the Pure term language.% \end{isamarkuptext}% \isamarkuptrue% % diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue Nov 18 18:25:10 2008 +0100 @@ -128,7 +128,7 @@ A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs \emph{within} the system itself, in conjunction with the document - preparation tools of Isabelle described in \cite{isabelle-sys}. + preparation tools of Isabelle described in \chref{ch:document-prep}. Thus partial or even wrong proof attempts can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} macros can be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/Thy/document/Symbols.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/document/Symbols.tex Tue Nov 18 18:25:10 2008 +0100 @@ -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:document-prep}. + + \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 c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/IsarRef/isar-ref.tex Tue Nov 18 18:25:10 2008 +0100 @@ -2,7 +2,14 @@ %% $Id$ \documentclass[12pt,a4paper,fleqn]{report} -\usepackage{latexsym,graphicx} +\usepackage{amssymb} +\usepackage[greek,english]{babel} +\usepackage[latin1]{inputenc} +\usepackage[only,bigsqcap]{stmaryrd} +\usepackage{textcomp} +\usepackage{latexsym} +\usepackage{graphicx} +\let\intorig=\int %iman.sty redefines \int \usepackage{../iman,../extra,../isar,../proof} \usepackage[nohyphen,strings]{../underscore} \usepackage{../isabelle,../isabellesym} @@ -89,6 +96,8 @@ \appendix \input{Thy/document/Quick_Reference.tex} +\let\int\intorig +\input{Thy/document/Symbols.tex} \input{Thy/document/ML_Tactic.tex} \begingroup diff -r c6b17889237a -r d5db6dfcb34a doc-src/IsarRef/showsymbols --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/showsymbols Tue Nov 18 18:25:10 2008 +0100 @@ -0,0 +1,28 @@ +#!/usr/bin/env perl +# +# $Id$ + +print "\\begin{supertabular}{ll\@{\\qquad}ll}\n"; + +$eol = "&"; + +while () { + if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) { + print "\\verb,\\<$1>, & {\\isasym$1} $eol\n"; +# print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n"; +# print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n"; +# print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n"; + if ("$eol" eq "&") { + $eol = "\\\\"; + } else { + $eol = "&"; + } + } +} + +if ("$eol" eq "\\\\") { + print "$eol\n"; +} + +print "\\end{supertabular}\n"; + diff -r c6b17889237a -r d5db6dfcb34a doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/System/IsaMakefile Tue Nov 18 18:25:10 2008 +0100 @@ -22,7 +22,7 @@ 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 Thy/Symbols.thy + Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy @$(USEDIR) -s System Pure Thy diff -r c6b17889237a -r d5db6dfcb34a doc-src/System/Makefile --- a/doc-src/System/Makefile Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/System/Makefile Tue Nov 18 18:25:10 2008 +0100 @@ -13,16 +13,12 @@ NAME = system 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 - @./showsymbols <../isabellesym.sty >syms.tex + Thy/document/Presentation.tex ../iman.sty ../extra.sty \ + ../ttbox.sty ../manual.bib dvi: $(NAME).dvi -$(NAME).dvi: $(FILES) isabelle.eps syms.tex +$(NAME).dvi: $(FILES) isabelle.eps $(LATEX) $(NAME) $(BIBTEX) $(NAME) $(LATEX) $(NAME) @@ -32,7 +28,7 @@ pdf: $(NAME).pdf -$(NAME).pdf: $(FILES) isabelle.pdf syms.tex +$(NAME).pdf: $(FILES) isabelle.pdf $(PDFLATEX) $(NAME) $(BIBTEX) $(NAME) $(PDFLATEX) $(NAME) diff -r c6b17889237a -r d5db6dfcb34a doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/System/Thy/Presentation.thy Tue Nov 18 18:25:10 2008 +0100 @@ -686,8 +686,8 @@ "isabellesym.sty"} should be included as well. This package contains a standard set of {\LaTeX} macro definitions @{verbatim "\\isasym"}@{text foo} corresponding to @{verbatim "\\"}@{verbatim - "<"}@{text foo}@{verbatim ">"}, (see \appref{app:symbols} for a - complete list of predefined Isabelle symbols). Users may invent + "<"}@{text foo}@{verbatim ">"}, see \cite{isabelle-implementation} for a + complete list of predefined Isabelle symbols. Users may invent further symbols as well, just by providing {\LaTeX} macros in a similar fashion as in @{"file" "~~/lib/texinputs/isabellesym.sty"} of the distribution. diff -r c6b17889237a -r d5db6dfcb34a doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/System/Thy/ROOT.ML Tue Nov 18 18:25:10 2008 +0100 @@ -7,4 +7,3 @@ use_thy "Basics"; use_thy "Presentation"; use_thy "Misc"; -use_thy "Symbols"; diff -r c6b17889237a -r d5db6dfcb34a doc-src/System/Thy/Symbols.thy --- a/doc-src/System/Thy/Symbols.thy Tue Nov 18 18:22:49 2008 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,49 +0,0 @@ -(* $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 c6b17889237a -r d5db6dfcb34a doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/System/Thy/document/Presentation.tex Tue Nov 18 18:25:10 2008 +0100 @@ -694,8 +694,8 @@ If the text contains any references to Isabelle symbols (such as \verb|\|\verb||) then \verb|isabellesym.sty| should be included as well. This package - contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, (see \appref{app:symbols} for a - complete list of predefined Isabelle symbols). Users may invent + contains a standard set of {\LaTeX} macro definitions \verb|\isasym|\isa{foo} corresponding to \verb|\|\verb|<|\isa{foo}\verb|>|, see \cite{isabelle-implementation} for a + complete list of predefined Isabelle symbols. Users may invent further symbols as well, just by providing {\LaTeX} macros in a similar fashion as in \hyperlink{file.~~/lib/texinputs/isabellesym.sty}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}lib{\isacharslash}texinputs{\isacharslash}isabellesym{\isachardot}sty}}}} of the distribution. diff -r c6b17889237a -r d5db6dfcb34a doc-src/System/Thy/document/Symbols.tex --- a/doc-src/System/Thy/document/Symbols.tex Tue Nov 18 18:22:49 2008 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,75 +0,0 @@ -% -\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 c6b17889237a -r d5db6dfcb34a doc-src/System/showsymbols --- a/doc-src/System/showsymbols Tue Nov 18 18:22:49 2008 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -#!/usr/bin/env perl -# -# $Id$ - -print "\\begin{supertabular}{ll\@{\\qquad}ll}\n"; - -$eol = "&"; - -while () { - if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) { - print "\\verb,\\<$1>, & {\\isasym$1} $eol\n"; -# print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n"; -# print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n"; -# print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n"; - if ("$eol" eq "&") { - $eol = "\\\\"; - } else { - $eol = "&"; - } - } -} - -if ("$eol" eq "\\\\") { - print "$eol\n"; -} - -print "\\end{supertabular}\n"; - diff -r c6b17889237a -r d5db6dfcb34a doc-src/System/system.tex --- a/doc-src/System/system.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/System/system.tex Tue Nov 18 18:25:10 2008 +0100 @@ -2,13 +2,7 @@ %% $Id$ \documentclass[12pt,a4paper]{report} -\usepackage{amssymb} -\usepackage[greek,english]{babel} -\usepackage[latin1]{inputenc} -\usepackage[only,bigsqcap]{stmaryrd} -\usepackage{textcomp} \usepackage{supertabular} -\let\intorig=\int %iman.sty redefines \int \usepackage{graphicx} \usepackage{../iman,../extra,../isar,../ttbox} \usepackage[nohyphen,strings]{../underscore} @@ -36,13 +30,9 @@ \maketitle \pagenumbering{roman} \tableofcontents \clearfirst -\input{Thy/document/Basics} -\input{Thy/document/Presentation} -\input{Thy/document/Misc} - -\appendix -\let\int\intorig -\input{Thy/document/Symbols} +\input{Thy/document/Basics.tex} +\input{Thy/document/Presentation.tex} +\input{Thy/document/Misc.tex} \begingroup \bibliographystyle{plain} \small\raggedright\frenchspacing diff -r c6b17889237a -r d5db6dfcb34a doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Tue Nov 18 18:25:10 2008 +0100 @@ -119,7 +119,7 @@ its definition is found in theorem \isa{o{\isacharunderscore}def}). \end{exercise} \begin{exercise}\label{ex:trev-trev} - Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ term} + Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}\ {\isacharprime}f{\isacharparenright}\ Nested{\isachardot}term} that recursively reverses the order of arguments of all function symbols in a term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}. \end{exercise} diff -r c6b17889237a -r d5db6dfcb34a doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/TutorialI/Documents/Documents.thy Tue Nov 18 18:25:10 2008 +0100 @@ -107,7 +107,7 @@ \verb,\,\verb,, symbol as~@{text \}. A list of standard Isabelle symbols is given in - \cite[appendix~A]{isabelle-sys}. You may introduce your own + \cite{isabelle-isar-ref}. You may introduce your own interpretation of further symbols by configuring the appropriate front-end tool accordingly, e.g.\ by defining certain {\LaTeX} macros (see also \S\ref{sec:doc-prep-symbols}). There are also a @@ -666,7 +666,7 @@ straightforward generalization of ASCII characters. While Isabelle does not impose any interpretation of the infinite collection of named symbols, {\LaTeX} documents use canonical glyphs for certain - standard symbols \cite[appendix~A]{isabelle-sys}. + standard symbols \cite{isabelle-isar-ref}. The {\LaTeX} code produced from Isabelle text follows a simple scheme. You can tune the final appearance by redefining certain diff -r c6b17889237a -r d5db6dfcb34a doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Tue Nov 18 18:25:10 2008 +0100 @@ -123,7 +123,7 @@ \verb,\,\verb,, symbol as~\isa{{\isasymforall}}. A list of standard Isabelle symbols is given in - \cite[appendix~A]{isabelle-sys}. You may introduce your own + \cite{isabelle-isar-ref}. You may introduce your own interpretation of further symbols by configuring the appropriate front-end tool accordingly, e.g.\ by defining certain {\LaTeX} macros (see also \S\ref{sec:doc-prep-symbols}). There are also a @@ -394,18 +394,18 @@ (usually rooted at \verb,~/isabelle/browser_info,). \medskip The easiest way to manage Isabelle sessions is via - \texttt{isatool mkdir} (generates an initial session source setup) - and \texttt{isatool make} (run sessions controlled by + \texttt{isabelle mkdir} (generates an initial session source setup) + and \texttt{isabelle make} (run sessions controlled by \texttt{IsaMakefile}). For example, a new session \texttt{MySession} derived from \texttt{HOL} may be produced as follows: \begin{verbatim} - isatool mkdir HOL MySession - isatool make + isabelle mkdir HOL MySession + isabelle make \end{verbatim} - The \texttt{isatool make} job also informs about the file-system + The \texttt{isabelle make} job also informs about the file-system location of the ultimate results. The above dry run should be able to produce some \texttt{document.pdf} (with dummy title, empty table of contents etc.). Any failure at this stage usually indicates @@ -441,7 +441,7 @@ several sessions may be managed by the same \texttt{IsaMakefile}. See the \emph{Isabelle System Manual} \cite{isabelle-sys} for further details, especially on - \texttt{isatool usedir} and \texttt{isatool make}. + \texttt{isabelle usedir} and \texttt{isabelle make}. \end{itemize} @@ -464,7 +464,7 @@ \texttt{MySession/document} directory as well. In particular, adding a file named \texttt{root.bib} causes an automatic run of \texttt{bibtex} to process a bibliographic database; see also - \texttt{isatool document} \cite{isabelle-sys}. + \texttt{isabelle document} \cite{isabelle-sys}. \medskip Any failure of the document preparation phase in an Isabelle batch session leaves the generated sources in their target @@ -741,7 +741,7 @@ straightforward generalization of ASCII characters. While Isabelle does not impose any interpretation of the infinite collection of named symbols, {\LaTeX} documents use canonical glyphs for certain - standard symbols \cite[appendix~A]{isabelle-sys}. + standard symbols \cite{isabelle-isar-ref}. The {\LaTeX} code produced from Isabelle text follows a simple scheme. You can tune the final appearance by redefining certain @@ -844,7 +844,7 @@ tagged region, in order to keep, drop, or fold the corresponding parts of the document. See the \emph{Isabelle System Manual} \cite{isabelle-sys} for further details, especially on - \texttt{isatool usedir} and \texttt{isatool document}. + \texttt{isabelle usedir} and \texttt{isabelle document}. Ignored material is specified by delimiting the original formal source with special source comments diff -r c6b17889237a -r d5db6dfcb34a doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Nov 18 18:22:49 2008 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Nov 18 18:25:10 2008 +0100 @@ -569,9 +569,7 @@ effect of show sorts on the above \begin{isabelle}% -{\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline -\isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline -{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% +{\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% \end{isabelle} \rulename{mult_cancel_left}% \end{isamarkuptext}%