138 |
138 |
139 |
139 |
140 subsubsection \<open>Examples\<close> |
140 subsubsection \<open>Examples\<close> |
141 |
141 |
142 text \<open> |
142 text \<open> |
143 See @{file "~~/src/HOL/ROOT"} for a diversity of practically relevant |
143 See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations, |
144 situations, although it uses relatively complex quasi-hierarchic naming |
144 although it uses relatively complex quasi-hierarchic naming conventions like |
145 conventions like \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to |
145 \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified |
146 use unqualified names that are relatively long and descriptive, as in the |
146 names that are relatively long and descriptive, as in the Archive of Formal |
147 Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for |
147 Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example. |
148 example. |
|
149 \<close> |
148 \<close> |
150 |
149 |
151 |
150 |
152 section \<open>System build options \label{sec:system-options}\<close> |
151 section \<open>System build options \label{sec:system-options}\<close> |
153 |
152 |
154 text \<open> |
153 text \<open> |
155 See @{file "~~/etc/options"} for the main defaults provided by the Isabelle |
154 See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle |
156 distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple |
155 distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple |
157 editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format. |
156 editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format. |
158 |
157 |
159 The following options are particularly relevant to build Isabelle sessions, |
158 The following options are particularly relevant to build Isabelle sessions, |
160 in particular with document preparation (\chref{ch:present}). |
159 in particular with document preparation (\chref{ch:present}). |