src/Doc/System/Presentation.thy
changeset 63680 6e1e8b5abbfa
parent 63669 256fc20716f2
child 67042 677cab7c2b85
     1.1 --- a/src/Doc/System/Presentation.thy	Fri Aug 12 17:49:02 2016 +0200
     1.2 +++ b/src/Doc/System/Presentation.thy	Fri Aug 12 17:53:55 2016 +0200
     1.3 @@ -69,9 +69,9 @@
     1.4    The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
     1.5    reported by the above verbose invocation of the build process.
     1.6  
     1.7 -  Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{dir
     1.8 -  "~~/src/HOL/Library"}) also provide printable documents in PDF. These are
     1.9 -  prepared automatically as well if enabled like this:
    1.10 +  Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in \<^dir>\<open>~~/src/HOL/Library\<close>)
    1.11 +  also provide printable documents in PDF. These are prepared automatically as
    1.12 +  well if enabled like this:
    1.13    @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
    1.14  
    1.15    Enabling both browser info and document preparation simultaneously causes an
    1.16 @@ -177,8 +177,8 @@
    1.17    drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
    1.18    equivalent to the tag specification
    1.19    ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
    1.20 -  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in @{file
    1.21 -  "~~/lib/texinputs/isabelle.sty"}.
    1.22 +  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
    1.23 +  \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
    1.24  
    1.25    \<^medskip>
    1.26    Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
    1.27 @@ -211,8 +211,8 @@
    1.28    user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
    1.29    theories.
    1.30  
    1.31 -  The {\LaTeX} versions of the theories require some macros defined in @{file
    1.32 -  "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
    1.33 +  The {\LaTeX} versions of the theories require some macros defined in
    1.34 +  \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
    1.35    \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
    1.36    appropriate path specification for {\TeX} inputs.
    1.37  
    1.38 @@ -221,11 +221,11 @@
    1.39    standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
    1.40    \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
    1.41    of predefined Isabelle symbols. Users may invent further symbols as well,
    1.42 -  just by providing {\LaTeX} macros in a similar fashion as in @{file
    1.43 -  "~~/lib/texinputs/isabellesym.sty"} of the Isabelle distribution.
    1.44 +  just by providing {\LaTeX} macros in a similar fashion as in
    1.45 +  \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
    1.46  
    1.47    For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
    1.48 -  we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well.
    1.49 +  we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
    1.50  
    1.51    \<^medskip>
    1.52    As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is