--- a/src/Doc/Codegen/Adaptation.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Fri Aug 12 17:53:55 2016 +0200
@@ -154,7 +154,7 @@
The @{theory HOL} @{theory Main} theory already provides a code
generator setup which should be suitable for most applications.
Common extensions and modifications are available by certain
- theories in @{dir "~~/src/HOL/Library"}; beside being useful in
+ theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in
applications, they may serve as a tutorial for customising the code
generator setup (see below \secref{sec:adaptation_mechanisms}).
--- a/src/Doc/Codegen/Further.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Codegen/Further.thy Fri Aug 12 17:53:55 2016 +0200
@@ -148,7 +148,7 @@
subsection \<open>Parallel computation\<close>
text \<open>
- Theory @{text Parallel} in @{dir "~~/src/HOL/Library"} contains
+ Theory @{text Parallel} in \<^dir>\<open>~~/src/HOL/Library\<close> contains
operations to exploit parallelism inside the Isabelle/ML
runtime engine.
\<close>
--- a/src/Doc/Codegen/Inductive_Predicate.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Fri Aug 12 17:53:55 2016 +0200
@@ -262,7 +262,7 @@
text \<open>
Further examples for compiling inductive predicates can be found in
- @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}. There are
+ \<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>. There are
also some examples in the Archive of Formal Proofs, notably in the
@{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
sessions.
--- a/src/Doc/Corec/Corec.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Corec/Corec.thy Fri Aug 12 17:53:55 2016 +0200
@@ -22,7 +22,7 @@
text \<open>
Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient
syntax for introducing codatatypes. For example, the type of (infinite) streams
-can be defined as follows (cf. @{file "~~/src/HOL/Library/Stream.thy"}):
+can be defined as follows (cf. \<^file>\<open>~~/src/HOL/Library/Stream.thy\<close>):
\<close>
codatatype 'a stream =
@@ -38,7 +38,7 @@
@{command corecursive}, @{command friend_of_corec}, and @{command coinduction_upto}.
It also covers the @{method corec_unique} proof method.
The package is not part of @{theory Main}; it is located in
-@{file "~~/src/HOL/Library/BNF_Corec.thy"}.
+\<^file>\<open>~~/src/HOL/Library/BNF_Corec.thy\<close>.
The @{command corec} command generalizes \keyw{primcorec} in three main
respects. First, it allows multiple constructors around corecursive calls, where
@@ -127,7 +127,7 @@
text \<open>
The package is illustrated through concrete examples featuring different flavors
of corecursion. More examples can be found in the directory
-@{dir "~~/src/HOL/Corec_Examples"}.
+\<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
\<close>
@@ -368,7 +368,7 @@
text \<open>
A more elaborate case study, revolving around the filter function on lazy lists,
-is presented in @{file "~~/src/HOL/Corec_Examples/LFilter.thy"}.
+is presented in \<^file>\<open>~~/src/HOL/Corec_Examples/LFilter.thy\<close>.
\<close>
--- a/src/Doc/Datatypes/Datatypes.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Aug 12 17:53:55 2016 +0200
@@ -78,7 +78,7 @@
infinite branching.
The package is part of @{theory Main}. Additional functionality is provided by
-the theory @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"}.
+the theory \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.
The package, like its predecessor, fully adheres to the LCF philosophy
@{cite mgordon79}: The characteristic theorems associated with the specified
@@ -163,7 +163,7 @@
text \<open>
Datatypes are illustrated through concrete examples featuring different flavors
of recursion. More examples can be found in the directory
-@{dir "~~/src/HOL/Datatype_Examples"}.
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
\<close>
@@ -1138,7 +1138,7 @@
\label{sssec:datatype-compat}\<close>
text \<open>
-The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a
+The theory \<^file>\<open>~~/src/HOL/Library/Countable.thy\<close> provides a
proof method called @{method countable_datatype} that can be used to prove the
countability of many datatypes, building on the countability of the types
appearing in their definitions and of any type arguments. For example:
@@ -1218,7 +1218,7 @@
\end{itemize}
The old command is still available as \keyw{old_datatype} in theory
-@{file "~~/src/HOL/Library/Old_Datatype.thy"}. However, there is no general
+\<^file>\<open>~~/src/HOL/Library/Old_Datatype.thy\<close>. However, there is no general
way to register old-style datatypes as new-style datatypes. If the objective
is to define new-style datatypes with nested recursion through old-style
datatypes, the old-style datatypes can be registered as a BNF
@@ -1247,7 +1247,7 @@
text \<open>
Primitive recursion is illustrated through concrete examples based on the
datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
-examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
\<close>
@@ -1320,7 +1320,7 @@
Pattern matching is only available for the argument on which the recursion takes
place. Fortunately, it is easy to generate pattern-maching equations using the
@{command simps_of_case} command provided by the theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
\<close>
simps_of_case at_simps_alt: at.simps
@@ -1760,7 +1760,7 @@
Codatatypes can be specified using the @{command codatatype} command. The
command is first illustrated through concrete examples featuring different
flavors of corecursion. More examples can be found in the directory
-@{dir "~~/src/HOL/Datatype_Examples"}. The \emph{Archive of Formal Proofs} also
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>. The \emph{Archive of Formal Proofs} also
includes some useful codatatypes, notably for lazy lists @{cite
"lochbihler-2010"}.
\<close>
@@ -2038,7 +2038,7 @@
on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
\keyw{corecursive} are described in a separate tutorial
@{cite "isabelle-corec"}. More examples can be found in the directories
-@{dir "~~/src/HOL/Datatype_Examples"} and @{dir "~~/src/HOL/Corec_Examples"}.
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close> and \<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
Whereas recursive functions consume datatypes one constructor at a time,
corecursive functions construct codatatypes one constructor at a time.
@@ -2082,7 +2082,7 @@
text \<open>
Primitive corecursion is illustrated through concrete examples based on the
codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
-examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
The code view is favored in the examples below. Sections
\ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
present the same examples expressed using the constructor and destructor views.
@@ -2143,7 +2143,7 @@
Pattern matching is not supported by @{command primcorec}. Fortunately, it is
easy to generate pattern-maching equations using the @{command simps_of_case}
-command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
+command provided by the theory \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
\<close>
simps_of_case lapp_simps: lapp.code
@@ -2776,7 +2776,7 @@
text \<open>
The example below shows how to register a type as a BNF using the @{command bnf}
command. Some of the proof obligations are best viewed with the theory
-@{file "~~/src/HOL/Library/Cardinal_Notations.thy"} imported.
+\<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
is live and @{typ 'd} is dead. We introduce it together with its map function,
@@ -2875,10 +2875,10 @@
This particular example does not need any nonemptiness witness, because the
one generated by default is good enough, but in general this would be
-necessary. See @{file "~~/src/HOL/Basic_BNFs.thy"},
-@{file "~~/src/HOL/Library/Countable_Set_Type.thy"},
-@{file "~~/src/HOL/Library/FSet.thy"}, and
-@{file "~~/src/HOL/Library/Multiset.thy"} for further examples of BNF
+necessary. See \<^file>\<open>~~/src/HOL/Basic_BNFs.thy\<close>,
+\<^file>\<open>~~/src/HOL/Library/Countable_Set_Type.thy\<close>,
+\<^file>\<open>~~/src/HOL/Library/FSet.thy\<close>, and
+\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for further examples of BNF
registration, some of which feature custom witnesses.
For many typedefs, lifting the BNF structure from the raw type to the abstract
@@ -3107,7 +3107,7 @@
The command is useful to reason abstractly about BNFs. The axioms are safe
because there exist BNFs of arbitrary large arities. Applications must import
-the @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"} theory
+the \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close> theory
to use this functionality.
\<close>
@@ -3210,7 +3210,7 @@
\noindent
The @{command simps_of_case} command provided by theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a single equation with
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a single equation with
a complex case expression on the right-hand side into a set of pattern-matching
equations. For example,
\<close>
@@ -3249,7 +3249,7 @@
\noindent
The \keyw{case_of_simps} command provided by theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a set of
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a set of
pattern-matching equations into single equation with a complex case expression
on the right-hand side (cf.\ @{command simps_of_case}). For example,
\<close>
@@ -3386,7 +3386,7 @@
@{text "('a\<^sub>1 \<Rightarrow> nat) \<Rightarrow> \<dots> \<Rightarrow> ('a\<^sub>m \<Rightarrow> nat) \<Rightarrow> u \<Rightarrow> nat"} using
the ML function @{ML BNF_LFP_Size.register_size} or
@{ML BNF_LFP_Size.register_size_global}. See theory
-@{file "~~/src/HOL/Library/Multiset.thy"} for an example.
+\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for an example.
\<close>
--- a/src/Doc/Implementation/Eq.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/Eq.thy Fri Aug 12 17:53:55 2016 +0200
@@ -64,10 +64,10 @@
@{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
\end{mldecls}
- See also @{file "~~/src/Pure/thm.ML" } for further description of these
- inference rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note
- that \<open>\<alpha>\<close> conversion is implicit due to the representation of terms with
- de-Bruijn indices (\secref{sec:terms}).
+ See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
+ rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close>
+ conversion is implicit due to the representation of terms with de-Bruijn
+ indices (\secref{sec:terms}).
\<close>
--- a/src/Doc/Implementation/Integration.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/Integration.thy Fri Aug 12 17:53:55 2016 +0200
@@ -132,9 +132,9 @@
\<close>
text %mlex \<open>
- The file @{file "~~/src/HOL/ex/Commands.thy"} shows some example Isar
- command definitions, with the all-important theory header declarations for
- outer syntax keywords.
+ The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command
+ definitions, with the all-important theory header declarations for outer
+ syntax keywords.
\<close>
--- a/src/Doc/Implementation/Logic.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/Logic.thy Fri Aug 12 17:53:55 2016 +0200
@@ -1248,11 +1248,11 @@
\<close>
text %mlex \<open>
- \<^item> @{file "~~/src/HOL/Proofs/ex/Proof_Terms.thy"} provides basic examples
- involving proof terms.
+ \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close> provides basic examples involving
+ proof terms.
- \<^item> @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} demonstrates export and import
- of proof terms via XML/ML data representation.
+ \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/XML_Data.thy\<close> demonstrates export and import of
+ proof terms via XML/ML data representation.
\<close>
end
--- a/src/Doc/Implementation/ML.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Fri Aug 12 17:53:55 2016 +0200
@@ -22,8 +22,8 @@
The main aspects of Isabelle/ML are introduced below. These first-hand
explanations should help to understand how proper Isabelle/ML is to be read
and written, and to get access to the wealth of experience that is expressed
- in the source text and its history of changes.\<^footnote>\<open>See @{url
- "http://isabelle.in.tum.de/repos/isabelle"} for the full Mercurial history.
+ in the source text and its history of changes.\<^footnote>\<open>See
+ \<^url>\<open>http://isabelle.in.tum.de/repos/isabelle\<close> for the full Mercurial history.
There are symbolic tags to refer to official Isabelle releases, as opposed
to arbitrary \<^emph>\<open>tip\<close> versions that merely reflect snapshots that are never
really up-to-date.\<close>
@@ -38,9 +38,8 @@
really going on and how things really work. This is a non-trivial aim, but
it is supported by a certain style of writing Isabelle/ML that has emerged
from long years of system development.\<^footnote>\<open>See also the interesting style guide
- for OCaml @{url
- "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"} which shares
- many of our means and ends.\<close>
+ for OCaml \<^url>\<open>http://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
+ which shares many of our means and ends.\<close>
The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single
author of a small program this merely means ``choose your style and stick to
@@ -63,8 +62,8 @@
text \<open>
Isabelle source files have a certain standardized header format (with
precise spacing) that follows ancient traditions reaching back to the
- earliest versions of the system by Larry Paulson. See @{file
- "~~/src/Pure/thm.ML"}, for example.
+ earliest versions of the system by Larry Paulson. See
+ \<^file>\<open>~~/src/Pure/thm.ML\<close>, for example.
The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a
prose description of the purpose of the module. The latter can range from a
@@ -1385,8 +1384,8 @@
32-bit Poly/ML, and much higher for 64-bit systems.\<close>
Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
- @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
- "~~/src/Pure/General/integer.ML"} provides some additional operations.
+ @{ML_structure Int}. Structure @{ML_structure Integer} in
+ \<^file>\<open>~~/src/Pure/General/integer.ML\<close> provides some additional operations.
\<close>
@@ -1445,8 +1444,7 @@
text \<open>
Apart from @{ML Option.map} most other operations defined in structure
@{ML_structure Option} are alien to Isabelle/ML and never used. The
- operations shown above are defined in @{file
- "~~/src/Pure/General/basics.ML"}.
+ operations shown above are defined in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>.
\<close>
@@ -1474,9 +1472,9 @@
is required.
\<^descr> @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat lists as a
- set-like container that maintains the order of elements. See @{file
- "~~/src/Pure/library.ML"} for the full specifications (written in ML). There
- are some further derived operations like @{ML union} or @{ML inter}.
+ set-like container that maintains the order of elements. See
+ \<^file>\<open>~~/src/Pure/library.ML\<close> for the full specifications (written in ML).
+ There are some further derived operations like @{ML union} or @{ML inter}.
Note that @{ML insert} is conservative about elements that are already a
@{ML member} of the list, while @{ML update} ensures that the latest entry
@@ -1518,8 +1516,8 @@
fold_rev} attempts to preserve the order of elements in the result.
This way of merging lists is typical for context data
- (\secref{sec:context-data}). See also @{ML merge} as defined in @{file
- "~~/src/Pure/library.ML"}.
+ (\secref{sec:context-data}). See also @{ML merge} as defined in
+ \<^file>\<open>~~/src/Pure/library.ML\<close>.
\<close>
@@ -1555,8 +1553,8 @@
Association lists are adequate as simple implementation of finite mappings
in many practical situations. A more advanced table structure is defined in
- @{file "~~/src/Pure/General/table.ML"}; that version scales easily to
- thousands or millions of elements.
+ \<^file>\<open>~~/src/Pure/General/table.ML\<close>; that version scales easily to thousands or
+ millions of elements.
\<close>
@@ -1782,8 +1780,7 @@
on the associated condition variable, and returns the result \<open>y\<close>.
There are some further variants of the @{ML Synchronized.guarded_access}
- combinator, see @{file "~~/src/Pure/Concurrent/synchronized.ML"} for
- details.
+ combinator, see \<^file>\<open>~~/src/Pure/Concurrent/synchronized.ML\<close> for details.
\<close>
text %mlex \<open>
@@ -1809,8 +1806,8 @@
text \<open>
\<^medskip>
- See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how to implement a mailbox
- as synchronized variable over a purely functional list.
+ See \<^file>\<open>~~/src/Pure/Concurrent/mailbox.ML\<close> how to implement a mailbox as
+ synchronized variable over a purely functional list.
\<close>
--- a/src/Doc/Implementation/Tactic.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Implementation/Tactic.thy Fri Aug 12 17:53:55 2016 +0200
@@ -168,9 +168,8 @@
\end{mldecls}
\<^descr> Type @{ML_type tactic} represents tactics. The well-formedness conditions
- described above need to be observed. See also @{file
- "~~/src/Pure/General/seq.ML"} for the underlying implementation of lazy
- sequences.
+ described above need to be observed. See also \<^file>\<open>~~/src/Pure/General/seq.ML\<close>
+ for the underlying implementation of lazy sequences.
\<^descr> Type @{ML_type "int -> tactic"} represents tactics with explicit subgoal
addressing, with well-formedness conditions as described above.
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Aug 12 17:53:55 2016 +0200
@@ -40,7 +40,7 @@
Markup commands provide a structured way to insert text into the document
generated from a theory. Each markup command takes a single @{syntax text}
argument, which is passed as argument to a corresponding {\LaTeX} macro. The
- default macros provided by @{file "~~/lib/texinputs/isabelle.sty"} can be
+ default macros provided by \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close> can be
redefined according to the needs of the underlying document and {\LaTeX}
styles.
@@ -420,8 +420,8 @@
text_raw} (\secref{sec:markup}) consist of plain text. Its internal
structure consists of paragraphs and (nested) lists, using special Isabelle
symbols and some rules for indentation and blank lines. This quasi-visual
- format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>@{url "http://commonmark.org"}\<close>, but the
- full complexity of that notation is avoided.
+ format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>, but the full
+ complexity of that notation is avoided.
This is a summary of the main principles of minimal Markdown in Isabelle:
@@ -495,8 +495,8 @@
\<^medskip>
Command tags merely produce certain markup environments for type-setting.
- The meaning of these is determined by {\LaTeX} macros, as defined in @{file
- "~~/lib/texinputs/isabelle.sty"} or by the document author. The Isabelle
+ The meaning of these is determined by {\LaTeX} macros, as defined in
+ \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close> or by the document author. The Isabelle
document preparation tools also provide some high-level options to specify
the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
corresponding parts of the text. Logic sessions may also specify ``document
@@ -517,8 +517,8 @@
\<close>}
The @{antiquotation rail} antiquotation allows to include syntax diagrams
- into Isabelle documents. {\LaTeX} requires the style file @{file
- "~~/lib/texinputs/railsetup.sty"}, which can be used via
+ into Isabelle documents. {\LaTeX} requires the style file
+ \<^file>\<open>~~/lib/texinputs/railsetup.sty\<close>, which can be used via
\<^verbatim>\<open>\usepackage{railsetup}\<close> in \<^verbatim>\<open>root.tex\<close>, for example.
The rail specification language is quoted here as Isabelle @{syntax string}
--- a/src/Doc/Isar_Ref/Framework.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy Fri Aug 12 17:53:55 2016 +0200
@@ -89,13 +89,13 @@
\<^medskip>
Concrete applications require another intermediate layer: an object-logic.
Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
- commonly used; elementary examples are given in the directory @{dir
- "~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh
+ commonly used; elementary examples are given in the directory
+ \<^dir>\<open>~~/src/HOL/Isar_Examples\<close>. Some examples demonstrate how to start a fresh
object-logic from Isabelle/Pure, and use Isar proofs from the very start,
despite the lack of advanced proof tools at such an early stage (e.g.\ see
- @{file "~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy"}). Isabelle/FOL
- @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work,
- but are much less developed.
+ \<^file>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
+ "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
+ much less developed.
In order to illustrate natural deduction in Isar, we shall subsequently
refer to the background theory and library of Isabelle/HOL. This includes
@@ -524,7 +524,7 @@
may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
methods semantically in Isabelle/ML. The Eisbach language allows to define
proof methods symbolically, as recursive expressions over existing methods
- @{cite "Matichuk-et-al:2014"}; see also @{dir "~~/src/HOL/Eisbach"}.
+ @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Aug 12 17:53:55 2016 +0200
@@ -538,8 +538,8 @@
\<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
from well-founded induction and completeness of patterns. This factors out
some operations that are done internally by the function package and makes
- them available separately. See @{file "~~/src/HOL/ex/Induction_Schema.thy"}
- for examples.
+ them available separately. See \<^file>\<open>~~/src/HOL/ex/Induction_Schema.thy\<close> for
+ examples.
\<close>
@@ -659,8 +659,8 @@
Adhoc overloading allows to overload a constant depending on its type.
Typically this involves the introduction of an uninterpreted constant (used
for input and output) and the addition of some variants (used internally).
- For examples see @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
- @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
+ For examples see \<^file>\<open>~~/src/HOL/ex/Adhoc_Overloading_Examples.thy\<close> and
+ \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
@{rail \<open>
(@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
@@ -1013,7 +1013,7 @@
subsubsection \<open>Examples\<close>
-text \<open>See @{file "~~/src/HOL/ex/Records.thy"}, for example.\<close>
+text \<open>See \<^file>\<open>~~/src/HOL/ex/Records.thy\<close>, for example.\<close>
section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
@@ -1411,28 +1411,26 @@
\<^descr> @{attribute (HOL) quot_map} registers a quotient map theorem, a theorem
showing how to ``lift'' quotients over type constructors. E.g.\ @{term
"Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image Rep)
- (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
- @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
- the involved type is BNF without dead variables.
+ (rel_set T)"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
+ \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
+ involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a
relator applied to an equality restricted by a predicate @{term P} (i.e.\
@{term "eq_onp P"}) is equal to a predicator applied to the @{term P}. The
combinator @{const eq_onp} is used for internal encoding of proper subtypes.
Such theorems allows the package to hide \<open>eq_onp\<close> from a user in a
- user-readable form of a respectfulness theorem. For examples see @{file
- "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
- property is proved automatically if the involved type is BNF without dead
- variables.
+ user-readable form of a respectfulness theorem. For examples see
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) "relator_mono"} registers a property describing a
monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
This property is needed for proving a stronger transfer rule in
@{command_def (HOL) "lift_definition"} when a parametricity theorem for the
raw term is specified and also for the reflexivity prover. For examples see
- @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
- This property is proved automatically if the involved type is BNF without
- dead variables.
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) "relator_distr"} registers a property describing a
distributivity of the relation composition and a relator. E.g.\ \<open>rel_set R
@@ -1443,9 +1441,9 @@
specified each direction separately and also register multiple theorems with
different set of assumptions. This attribute can be used only after the
monotonicity property was already registered by @{attribute (HOL)
- "relator_mono"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
- @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
- the involved type is BNF without dead variables.
+ "relator_mono"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
+ \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
+ involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from
the Lifting infrastructure and thus de-register the corresponding quotient.
@@ -1524,7 +1522,7 @@
"transfer_step"}+, @{method (HOL) "transfer_end"}) and @{method (HOL)
"transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, @{method
(HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}). For usage
- examples see @{file "~~/src/HOL/ex/Transfer_Debug.thy"}
+ examples see \<^file>\<open>~~/src/HOL/ex/Transfer_Debug.thy\<close>.
\<^descr> @{attribute (HOL) "untransferred"} proves the same equivalent theorem as
@{method (HOL) "transfer"} internally does.
@@ -1566,17 +1564,15 @@
relators of various type constructors, e.g. @{term "rel_set (op =) = (op
=)"}. The @{method (HOL) transfer} method uses these lemmas to infer
transfer rules for non-polymorphic constants on the fly. For examples see
- @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
- This property is proved automatically if the involved type is BNF without
- dead variables.
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
\<^descr> @{attribute_def (HOL) "relator_domain"} attribute collects rules
describing domains of relators by predicators. E.g.\ @{term "Domainp
(rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package to lift
- transfer domain rules through type constructors. For examples see @{file
- "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
- property is proved automatically if the involved type is BNF without dead
- variables.
+ transfer domain rules through type constructors. For examples see
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
Theoretical background can be found in @{cite
@@ -2082,14 +2078,13 @@
\<close>}
\<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
- @{cite "loveland-78"}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
- examples.
+ @{cite "loveland-78"}. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
\<^descr> @{method (HOL) metis} combines ordered resolution and ordered
paramodulation to find first-order (or mildly higher-order) proofs. The
first optional argument specifies a type encoding; see the Sledgehammer
- manual @{cite "isabelle-sledgehammer"} for details. The directory @{dir
- "~~/src/HOL/Metis_Examples"} contains several small theories developed to a
+ manual @{cite "isabelle-sledgehammer"} for details. The directory
+ \<^dir>\<open>~~/src/HOL/Metis_Examples\<close> contains several small theories developed to a
large extent using @{method (HOL) metis}.
\<close>
@@ -2168,7 +2163,7 @@
(*<*)end(*>*)
text \<open>
- See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
+ See also \<^file>\<open>~~/src/HOL/ex/Groebner_Examples.thy\<close>.
\<close>
@@ -2185,8 +2180,8 @@
\<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
"Bezem-Coquand:2005"}, which covers applications in confluence theory,
- lattice theory and projective geometry. See @{file
- "~~/src/HOL/ex/Coherent.thy"} for some examples.
+ lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/ex/Coherent.thy\<close>
+ for some examples.
\<close>
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Aug 12 17:53:55 2016 +0200
@@ -571,8 +571,8 @@
float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token},
and @{syntax (inner) cartouche} are not used in Pure. Object-logics may
implement numerals and string literals by adding appropriate syntax
- declarations, together with some translation functions (e.g.\ see @{file
- "~~/src/HOL/Tools/string_syntax.ML"}).
+ declarations, together with some translation functions (e.g.\ see
+ \<^file>\<open>~~/src/HOL/Tools/string_syntax.ML\<close>).
The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
(inner) float_const}, provide robust access to the respective tokens: the
--- a/src/Doc/Isar_Ref/Spec.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Aug 12 17:53:55 2016 +0200
@@ -1303,8 +1303,8 @@
the scope of the resulting theory.
- See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of defining
- a new primitive rule as oracle, and turning it into a proof method.
+ See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new
+ primitive rule as oracle, and turning it into a proof method.
\<close>
--- a/src/Doc/Isar_Ref/Synopsis.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Isar_Ref/Synopsis.thy Fri Aug 12 17:53:55 2016 +0200
@@ -214,7 +214,7 @@
section \<open>Calculational reasoning \label{sec:calculations-synopsis}\<close>
text \<open>
- For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
+ For example, see \<^file>\<open>~~/src/HOL/Isar_Examples/Group.thy\<close>.
\<close>
--- a/src/Doc/JEdit/JEdit.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy Fri Aug 12 17:53:55 2016 +0200
@@ -37,11 +37,10 @@
given up; instead there is direct support for editing of source text, with
rich formal markup for GUI rendering.
- \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>@{url "http://www.jedit.org"}\<close>
- implemented in Java\<^footnote>\<open>@{url "http://www.java.com"}\<close>. It is easily
- extensible by plugins written in any language that works on the JVM. In
- the context of Isabelle this is always Scala\<^footnote>\<open>@{url
- "http://www.scala-lang.org"}\<close>.
+ \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
+ implemented in Java\<^footnote>\<open>\<^url>\<open>http://www.java.com\<close>\<close>. It is easily extensible by
+ plugins written in any language that works on the JVM. In the context of
+ Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>http://www.scala-lang.org\<close>\<close>.
\<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
default user-interface for Isabelle. It targets both beginners and
@@ -214,7 +213,7 @@
additional keyboard shortcuts for Isabelle-specific functionality. Users may
change their keymap later, but need to copy some keyboard shortcuts manually
(see also @{path "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close>
- properties in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
+ properties in \<^file>\<open>$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props\<close>).
\<close>
@@ -271,8 +270,8 @@
The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
Isabelle/jEdit. This is only relevant for building from sources, which also
- requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from @{url
- "http://isabelle.in.tum.de/components"}. The official Isabelle release
+ requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
+ \<^url>\<open>http://isabelle.in.tum.de/components\<close>. The official Isabelle release
already includes a pre-built version of Isabelle/jEdit.
\<^bigskip>
@@ -468,8 +467,8 @@
``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
example. This symbol interpretation is specified by the Isabelle system
- distribution in @{file "$ISABELLE_HOME/etc/symbols"} and may be augmented by
- the user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
+ distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
+ user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
standard interpretation of finitely many symbols from the infinite
@@ -550,7 +549,7 @@
\<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
The following table is an extract of the information provided by the
- standard @{file "$ISABELLE_HOME/etc/symbols"} file:
+ standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file:
\<^medskip>
\begin{tabular}{lll}
@@ -659,9 +658,8 @@
platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
environment variables from the Isabelle process may be used freely, e.g.\
- @{file "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}. There
- are special shortcuts: @{dir "~"} for @{dir "$USER_HOME"} and @{dir "~~"}
- for @{dir "$ISABELLE_HOME"}.
+ \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special
+ shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
\<^medskip>
Since jEdit happens to support environment variables within file
@@ -848,8 +846,8 @@
further tricks to manage markup of ML files, such that Isabelle/HOL may be
edited conveniently in the Prover IDE on small machines with only 8\,GB of
main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
- at the top @{file "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
- "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
+ at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
+ \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.
Initially, before an auxiliary file is opened in the editor, the prover
reads its content from the physical file-system. After the file is opened
@@ -874,8 +872,8 @@
Warnings, errors, and other useful markup is attached directly to the
positions in the auxiliary file buffer, in the manner of standard IDEs. By
- using the load command @{command SML_file} as explained in @{file
- "$ISABELLE_HOME/src/Tools/SML/Examples.thy"}, Isabelle/jEdit may be used as
+ using the load command @{command SML_file} as explained in
+ \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be used as
fully-featured IDE for Standard ML, independently of theory or proof
development: the required theory merely serves as some kind of project file
for a collection of SML source modules.
@@ -1044,8 +1042,7 @@
\<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
regular expression, in the notation that is commonly used on the Java
- platform.\<^footnote>\<open>@{url
- "https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html"}\<close>
+ platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>
This may serve as an additional visual filter of the result.
\<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
@@ -1240,9 +1237,8 @@
text \<open>
The completion tables for Isabelle symbols (\secref{sec:symbols}) are
- determined statically from @{file "$ISABELLE_HOME/etc/symbols"} and
- @{path "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
- specification as follows:
+ determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and @{path
+ "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows:
\<^medskip>
\begin{tabular}{ll}
@@ -1272,13 +1268,12 @@
which do not allow arbitrary backslash sequences.
\<^medskip>
- Additional abbreviations may be specified in @{file
- "$ISABELLE_HOME/etc/abbrevs"} and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}.
- The file content follows general Isar outer syntax @{cite
- "isabelle-isar-ref"}. Abbreviations are specified as
- ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
- than just one symbol; otherwise the meaning is the same as a symbol
- specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
+ Additional abbreviations may be specified in \<^file>\<open>$ISABELLE_HOME/etc/abbrevs\<close>
+ and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows
+ general Isar outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are
+ specified as ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may
+ consist of more than just one symbol; otherwise the meaning is the same as a
+ symbol specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
"etc/symbols"}.
\<close>
@@ -1718,10 +1713,10 @@
text \<open>
Document text is internally structured in paragraphs and nested lists, using
- notation that is similar to Markdown\<^footnote>\<open>@{url "http://commonmark.org"}\<close>. There
- are special control symbols for items of different kinds of lists,
- corresponding to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This
- is illustrated in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
+ notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are
+ special control symbols for items of different kinds of lists, corresponding
+ to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated
+ in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
\begin{figure}[!htb]
\begin{center}
@@ -1781,7 +1776,7 @@
chapter \<open>ML debugging within the Prover IDE\<close>
text \<open>
- Isabelle/ML is based on Poly/ML\<^footnote>\<open>@{url "http://www.polyml.org"}\<close> and thus
+ Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>http://www.polyml.org\<close>\<close> and thus
benefits from the source-level debugger of that implementation of Standard
ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running
ML threads, inspect the stack frame with local ML bindings, and evaluate ML
--- a/src/Doc/Locales/Examples3.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy Fri Aug 12 17:53:55 2016 +0200
@@ -525,7 +525,7 @@
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
- @{url "http://isabelle.in.tum.de"}.
+ \<^url>\<open>http://isabelle.in.tum.de\<close>.
\<close>
text \<open>
--- a/src/Doc/Main/Main_Doc.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy Fri Aug 12 17:53:55 2016 +0200
@@ -26,7 +26,7 @@
text\<open>
\begin{abstract}
-This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see @{url "http://isabelle.in.tum.de/library/HOL/"}.
+This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>.
\end{abstract}
\section*{HOL}
--- a/src/Doc/Prog_Prove/Basics.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy Fri Aug 12 17:53:55 2016 +0200
@@ -124,9 +124,9 @@
\end{warn}
In addition to the theories that come with the Isabelle/HOL distribution
-(see @{url "http://isabelle.in.tum.de/library/HOL/"})
+(see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>)
there is also the \emph{Archive of Formal Proofs}
-at @{url "http://afp.sourceforge.net"}, a growing collection of Isabelle theories
+at \<^url>\<open>http://afp.sourceforge.net\<close>, a growing collection of Isabelle theories
that everybody can contribute to.
\subsection{Quotation Marks}
--- a/src/Doc/System/Environment.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/System/Environment.thy Fri Aug 12 17:53:55 2016 +0200
@@ -44,11 +44,10 @@
that the Isabelle executables either have to be run from their original
location in the distribution directory, or via the executable objects
created by the @{tool install} tool. Symbolic links are admissible, but a
- plain copy of the @{dir "$ISABELLE_HOME/bin"} files will not work!
+ plain copy of the \<^dir>\<open>$ISABELLE_HOME/bin\<close> files will not work!
- \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
- @{executable_ref bash} shell script with the auto-export option for
- variables enabled.
+ \<^enum> The file \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> is run as a @{executable_ref
+ bash} shell script with the auto-export option for variables enabled.
This file holds a rather long list of shell variable assignments, thus
providing the site-wide default settings. The Isabelle distribution
@@ -63,8 +62,8 @@
Thus individual users may override the site-wide defaults. Typically, a
user settings file contains only a few lines, with some assignments that
- are actually changed. Never copy the central @{file
- "$ISABELLE_HOME/etc/settings"} file!
+ are actually changed. Never copy the central
+ \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file!
Since settings files are regular GNU @{executable_def bash} scripts, one may
use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
@@ -138,7 +137,7 @@
\<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
of the @{executable isabelle} executable. Thus other tools and scripts need
- not assume that the @{dir "$ISABELLE_HOME/bin"} directory is on the current
+ not assume that the \<^dir>\<open>$ISABELLE_HOME/bin\<close> directory is on the current
search path of the shell.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
@@ -147,8 +146,8 @@
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
specify the underlying ML system to be used for Isabelle. There is only a
- fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
- "$ISABELLE_HOME/etc/settings"} file of the distribution).
+ fixed set of admissable @{setting ML_SYSTEM} names (see the
+ \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).
The actual compiler binary will be run from the directory @{setting
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
@@ -429,8 +428,8 @@
separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
indicates close of an element. Any other non-empty chunk consists of plain
- text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
- "~~/src/Pure/PIDE/yxml.scala"}.
+ text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or
+ \<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>.
YXML documents may be detected quickly by checking that the first two
characters are \<open>\<^bold>X\<^bold>Y\<close>.
--- a/src/Doc/System/Misc.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/System/Misc.thy Fri Aug 12 17:53:55 2016 +0200
@@ -34,8 +34,8 @@
Components are initialized as described in \secref{sec:components} in a
permissive manner, which can mark components as ``missing''. This state is
amended by letting @{tool "components"} download and unpack components that
- are published on the default component repository @{url
- "http://isabelle.in.tum.de/components/"} in particular.
+ are published on the default component repository
+ \<^url>\<open>http://isabelle.in.tum.de/components\<close> in particular.
Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
\<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
--- a/src/Doc/System/Presentation.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/System/Presentation.thy Fri Aug 12 17:53:55 2016 +0200
@@ -69,9 +69,9 @@
The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
reported by the above verbose invocation of the build process.
- Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{dir
- "~~/src/HOL/Library"}) also provide printable documents in PDF. These are
- prepared automatically as well if enabled like this:
+ Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in \<^dir>\<open>~~/src/HOL/Library\<close>)
+ also provide printable documents in PDF. These are prepared automatically as
+ well if enabled like this:
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
Enabling both browser info and document preparation simultaneously causes an
@@ -177,8 +177,8 @@
drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
equivalent to the tag specification
``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
- \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in @{file
- "~~/lib/texinputs/isabelle.sty"}.
+ \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
+ \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
\<^medskip>
Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
@@ -211,8 +211,8 @@
user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
theories.
- The {\LaTeX} versions of the theories require some macros defined in @{file
- "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
+ The {\LaTeX} versions of the theories require some macros defined in
+ \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
\<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
appropriate path specification for {\TeX} inputs.
@@ -221,11 +221,11 @@
standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, 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 Isabelle distribution.
+ just by providing {\LaTeX} macros in a similar fashion as in
+ \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
- we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well.
+ we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
\<^medskip>
As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
--- a/src/Doc/System/Scala.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/System/Scala.thy Fri Aug 12 17:53:55 2016 +0200
@@ -88,8 +88,8 @@
This assumes that the executable may be found via the @{setting PATH} from
the process environment: this is the case when Isabelle settings are active,
e.g.\ in the context of the main Isabelle tool wrapper
- \secref{sec:isabelle-tool}. Alternatively, the full @{file
- "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in expanded
+ \secref{sec:isabelle-tool}. Alternatively, the full
+ \<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
form.
\<close>
--- a/src/Doc/System/Sessions.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/System/Sessions.thy Fri Aug 12 17:53:55 2016 +0200
@@ -140,19 +140,18 @@
subsubsection \<open>Examples\<close>
text \<open>
- See @{file "~~/src/HOL/ROOT"} for a diversity of practically relevant
- situations, although it uses relatively complex quasi-hierarchic naming
- conventions like \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to
- use unqualified names that are relatively long and descriptive, as in the
- Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
- example.
+ See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
+ although it uses relatively complex quasi-hierarchic naming conventions like
+ \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
+ names that are relatively long and descriptive, as in the Archive of Formal
+ Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example.
\<close>
section \<open>System build options \label{sec:system-options}\<close>
text \<open>
- See @{file "~~/etc/options"} for the main defaults provided by the Isabelle
+ See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 12 17:53:55 2016 +0200
@@ -9152,8 +9152,8 @@
subsection \<open>Geometric progression\<close>
-text \<open>FIXME: Should one or more of these theorems be moved to @{file
-"~~/src/HOL/Set_Interval.thy"}, alongside \<open>geometric_sum\<close>?\<close>
+text \<open>FIXME: Should one or more of these theorems be moved to
+ \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
lemma sum_gp_basic:
fixes x :: "'a::ring_1"
--- a/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 12 17:53:55 2016 +0200
@@ -1654,8 +1654,8 @@
qed
text \<open>TODO: The following lemmas about adjoints should hold for any
-Hilbert space (i.e. complete inner product space).
-(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
+ Hilbert space (i.e. complete inner product space).
+ (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
\<close>
lemma adjoint_works:
--- a/src/HOL/Bali/Decl.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Bali/Decl.thy Fri Aug 12 17:53:55 2016 +0200
@@ -15,7 +15,7 @@
\item clarification and correction of some aspects of the package/access concept
(Also submitted as bug report to the Java Bug Database:
Bug Id: 4485402 and Bug Id: 4493343
- @{url "http://developer.java.sun.com/developer/bugParade/index.jshtml"}
+ \<^url>\<open>http://developer.java.sun.com/developer/bugParade/index.jshtml\<close>
)
\end{itemize}
simplifications:
--- a/src/HOL/Binomial.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Binomial.thy Fri Aug 12 17:53:55 2016 +0200
@@ -502,7 +502,7 @@
subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
-text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
+text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
context comm_semiring_1
begin
--- a/src/HOL/Groups.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Groups.thy Fri Aug 12 17:53:55 2016 +0200
@@ -602,7 +602,7 @@
\<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
Most of the used notions can also be looked up in
- \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
+ \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
\<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
\<close>
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy Fri Aug 12 17:53:55 2016 +0200
@@ -32,7 +32,7 @@
Axioms for fair trace inclusion proof support, not for the correctness proof
of refinement mappings!
- Note: Everything is superseded by @{file "LiveIOA.thy"}.
+ Note: Everything is superseded by \<^file>\<open>LiveIOA.thy\<close>.
\<close>
axiomatization where
--- a/src/HOL/HOLCF/IOA/Traces.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Traces.thy Fri Aug 12 17:53:55 2016 +0200
@@ -84,7 +84,7 @@
else branch prohibits it. However they can be \<open>sfair\<close> in the case when all
\<open>W\<close> are only finitely often enabled: Is this the right model?
- See @{file "LiveIOA.thy"} for solution conforming with the literature and
+ See \<^file>\<open>LiveIOA.thy\<close> for solution conforming with the literature and
superseding this one.
\<close>
--- a/src/HOL/Imperative_HOL/Ref.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Fri Aug 12 17:53:55 2016 +0200
@@ -10,8 +10,8 @@
text \<open>
Imperative reference operations; modeled after their ML counterparts.
- See @{url "http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html"}
- and @{url "http://www.smlnj.org/doc/Conversion/top-level-comparison.html"}
+ See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
+ and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
\<close>
subsection \<open>Primitives\<close>
--- a/src/HOL/Induct/Ordinals.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Induct/Ordinals.thy Fri Aug 12 17:53:55 2016 +0200
@@ -11,7 +11,7 @@
text \<open>
Some basic definitions of ordinal numbers. Draws an Agda
development (in Martin-L\"of type theory) by Peter Hancock (see
- @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
+ \<^url>\<open>http://www.dcs.ed.ac.uk/home/pgh/chat.html\<close>).
\<close>
datatype ordinal =
--- a/src/HOL/Isar_Examples/Cantor.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy Fri Aug 12 17:53:55 2016 +0200
@@ -13,8 +13,8 @@
text \<open>
Cantor's Theorem states that there is no surjection from
a set to its powerset. The proof works by diagonalization. E.g.\ see
- \<^item> @{url "http://mathworld.wolfram.com/CantorDiagonalMethod.html"}
- \<^item> @{url "https://en.wikipedia.org/wiki/Cantor's_diagonal_argument"}
+ \<^item> \<^url>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
+ \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
\<close>
theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
--- a/src/HOL/Isar_Examples/Hoare.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Aug 12 17:53:55 2016 +0200
@@ -16,7 +16,7 @@
The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
programs closely follows the existing tradition in Isabelle/HOL of
formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
- @{dir "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.
+ \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}.
\<close>
type_synonym 'a bexp = "'a set"
@@ -358,14 +358,14 @@
text \<open>
We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition
- for the Hoare Verification Condition Generator (see @{dir
- "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a
- proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to
- extract purely logical verification conditions. It is important to note that
- the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants
- beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the
- underlying tactic fails ungracefully if supplied with meta-variables or
- parameters, for example.
+ for the Hoare Verification Condition Generator (see \<^dir>\<open>~~/src/HOL/Hoare\<close>).
+ As far as we are concerned here, the result is a proof method \<open>hoare\<close>, which
+ may be applied to a Hoare Logic assertion to extract purely logical
+ verification conditions. It is important to note that the method requires
+ \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants beforehand.
+ Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the underlying
+ tactic fails ungracefully if supplied with meta-variables or parameters, for
+ example.
\<close>
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Fri Aug 12 17:53:55 2016 +0200
@@ -10,8 +10,8 @@
text \<open>
See also:
- \<^item> @{file "$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy"}
- \<^item> @{url "http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem"}
+ \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close>
+ \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close>
\<^item> Springer LNCS 828 (cover page)
\<close>
--- a/src/HOL/Library/Code_Test.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Library/Code_Test.thy Fri Aug 12 17:53:55 2016 +0200
@@ -53,9 +53,10 @@
and (Scala) "_.mkString(\"\")"
text \<open>
- Stripped-down implementations of Isabelle's XML tree with YXML encoding
- as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
- sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
+ Stripped-down implementations of Isabelle's XML tree with YXML encoding as
+ defined in \<^file>\<open>~~/src/Pure/PIDE/xml.ML\<close>, \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close>
+ sufficient to encode @{typ "Code_Evaluation.term"} as in
+ \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
\<close>
datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
@@ -113,8 +114,8 @@
where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
text \<open>
- Encoding @{typ Code_Evaluation.term} into XML trees
- as defined in @{file "~~/src/Pure/term_xml.ML"}
+ Encoding @{typ Code_Evaluation.term} into XML trees as defined in
+ \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
\<close>
definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
--- a/src/HOL/Library/Extended_Real.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Aug 12 17:53:55 2016 +0200
@@ -218,10 +218,8 @@
qed
text \<open>
-
-For more lemmas about the extended real numbers go to
- @{file "~~/src/HOL/Analysis/Extended_Real_Limits.thy"}
-
+ For more lemmas about the extended real numbers see
+ \<^file>\<open>~~/src/HOL/Analysis/Extended_Real_Limits.thy\<close>.
\<close>
subsection \<open>Definition and basic properties\<close>
--- a/src/HOL/Library/RBT_Impl.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Fri Aug 12 17:53:55 2016 +0200
@@ -551,8 +551,10 @@
lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
by (cases t rule: rbt_cases) auto
-text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
-at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
+text \<open>
+ The function definitions are based on the Haskell code by Stefan Kahrs
+ at \<^url>\<open>http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html\<close>.
+\<close>
fun
balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
--- a/src/HOL/Library/Set_Algebras.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Fri Aug 12 17:53:55 2016 +0200
@@ -13,7 +13,7 @@
text \<open>
This library lifts operations like addition and multiplication to sets. It
was designed to support asymptotic calculations. See the comments at the top
- of @{file "BigO.thy"}.
+ of \<^file>\<open>BigO.thy\<close>.
\<close>
instantiation set :: (plus) plus
--- a/src/HOL/Library/State_Monad.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Library/State_Monad.thy Fri Aug 12 17:53:55 2016 +0200
@@ -20,7 +20,7 @@
monads}, since a state is transformed single-threadedly).
To enter from the Haskell world,
- @{url "http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm"} makes
+ \<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
a good motivating start. Here we just sketch briefly how those
monads enter the game of Isabelle/HOL.
\<close>
@@ -145,7 +145,7 @@
"_sdo_block (_sdo_final e)" => "e"
text \<open>
- For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy"}.
+ For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>.
\<close>
end
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Fri Aug 12 17:53:55 2016 +0200
@@ -16,9 +16,8 @@
by Roshan James (Indiana University) and also by the lecture notes
written by Andy Pitts for his semantics course. See
- @{url "http://www.cs.indiana.edu/~rpjames/lm.pdf"}
- @{url "http://www.cl.cam.ac.uk/teaching/2001/Semantics/"}
-
+ \<^url>\<open>http://www.cs.indiana.edu/~rpjames/lm.pdf\<close>
+ \<^url>\<open>http://www.cl.cam.ac.uk/teaching/2001/Semantics\<close>
\<close>
atom_decl name
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Aug 12 17:53:55 2016 +0200
@@ -4,7 +4,7 @@
"~~/src/HOL/Library/Code_Prolog"
begin
-text \<open>An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"})\<close>
+text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
text \<open>The example (original in Haskell) was imported with Haskabelle and
manually slightly adapted.
\<close>
--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Aug 12 17:53:55 2016 +0200
@@ -1414,7 +1414,7 @@
Proof that @{const rel_pmf} preserves orders.
Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
Theoretical Computer Science 12(1):19--37, 1980,
- @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
+ \<^url>\<open>http://dx.doi.org/10.1016/0304-3975(80)90003-1\<close>
\<close>
lemma
--- a/src/HOL/Real.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Real.thy Fri Aug 12 17:53:55 2016 +0200
@@ -14,10 +14,10 @@
begin
text \<open>
- This theory contains a formalization of the real numbers as
- equivalence classes of Cauchy sequences of rationals. See
- @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
- construction using Dedekind cuts.
+ This theory contains a formalization of the real numbers as equivalence
+ classes of Cauchy sequences of rationals. See
+ \<^file>\<open>~~/src/HOL/ex/Dedekind_Real.thy\<close> for an alternative construction using
+ Dedekind cuts.
\<close>
--- a/src/HOL/Real_Vector_Spaces.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Aug 12 17:53:55 2016 +0200
@@ -2084,7 +2084,7 @@
text \<open>
Proof that Cauchy sequences converge based on the one from
- @{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
+ \<^url>\<open>http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html\<close>
\<close>
text \<open>
--- a/src/HOL/Rings.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Rings.thy Fri Aug 12 17:53:55 2016 +0200
@@ -538,7 +538,7 @@
\<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
Most of the used notions can also be looked up in
- \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
+ \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
\<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
\<close>
--- a/src/HOL/Series.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Series.thy Fri Aug 12 17:53:55 2016 +0200
@@ -817,7 +817,7 @@
text \<open>
Proof based on Analysis WebNotes: Chapter 07, Class 41
- @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
+ \<^url>\<open>http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm\<close>
\<close>
lemma Cauchy_product_sums:
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Aug 12 17:53:55 2016 +0200
@@ -199,10 +199,10 @@
(** invocation of Haskell interpreter **)
val narrowing_engine =
- File.read @{file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
+ File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\<close>
val pnf_narrowing_engine =
- File.read @{file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
+ File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\<close>
fun exec verbose code =
ML_Context.exec (fn () =>
--- a/src/HOL/Word/Word.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/Word/Word.thy Fri Aug 12 17:53:55 2016 +0200
@@ -14,7 +14,7 @@
Word_Miscellaneous
begin
-text \<open>See @{file "Examples/WordExamples.thy"} for examples.\<close>
+text \<open>See \<^file>\<open>Examples/WordExamples.thy\<close> for examples.\<close>
subsection \<open>Type definition\<close>
--- a/src/HOL/ex/ML.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/ex/ML.thy Fri Aug 12 17:53:55 2016 +0200
@@ -94,7 +94,7 @@
ML \<open>factorial 42\<close>
ML \<open>factorial 10000 div factorial 9999\<close>
-text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close>
+text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close>
ML \<open>
fun ackermann 0 n = n + 1
--- a/src/HOL/ex/NatSum.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/ex/NatSum.thy Fri Aug 12 17:53:55 2016 +0200
@@ -10,7 +10,7 @@
Summing natural numbers, squares, cubes, etc.
Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
- @{url "http://www.research.att.com/~njas/sequences/"}.
+ \<^url>\<open>http://www.research.att.com/~njas/sequences\<close>.
\<close>
lemmas [simp] =
--- a/src/HOL/ex/Simproc_Tests.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Fri Aug 12 17:53:55 2016 +0200
@@ -9,10 +9,9 @@
begin
text \<open>
- This theory tests the various simprocs defined in @{file
- "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
- Many of the tests are derived from commented-out code originally
- found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
+ This theory tests the various simprocs defined in \<^file>\<open>~~/src/HOL/Nat.thy\<close> and
+ \<^file>\<open>~~/src/HOL/Numeral_Simprocs.thy\<close>. Many of the tests are derived from commented-out code
+ originally found in \<^file>\<open>~~/src/HOL/Tools/numeral_simprocs.ML\<close>.
\<close>
subsection \<open>ML bindings\<close>
--- a/src/HOL/ex/Sudoku.thy Fri Aug 12 17:49:02 2016 +0200
+++ b/src/HOL/ex/Sudoku.thy Fri Aug 12 17:53:55 2016 +0200
@@ -136,7 +136,7 @@
text \<open>
Some ``exceptionally difficult'' Sudokus, taken from
- @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
+ \<^url>\<open>http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
(accessed December~2, 2008).
\<close>
--- a/src/Pure/Tools/jedit.ML Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Pure/Tools/jedit.ML Fri Aug 12 17:53:55 2016 +0200
@@ -24,13 +24,13 @@
val isabelle_jedit_actions =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/actions.xml"}) of
+ (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) of
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
| _ => []));
val isabelle_jedit_dockables =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/dockables.xml"}) of
+ (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
| _ => []));