1.1 --- a/src/Doc/IsarImplementation/ML.thy Mon Dec 09 12:16:52 2013 +0100
1.2 +++ b/src/Doc/IsarImplementation/ML.thy Mon Dec 09 12:22:23 2013 +0100
1.3 @@ -22,7 +22,7 @@
1.4 Isabelle/ML is to be read and written, and to get access to the
1.5 wealth of experience that is expressed in the source text and its
1.6 history of changes.\footnote{See
1.7 - \url{http://isabelle.in.tum.de/repos/isabelle} for the full
1.8 + @{url "http://isabelle.in.tum.de/repos/isabelle"} for the full
1.9 Mercurial history. There are symbolic tags to refer to official
1.10 Isabelle releases, as opposed to arbitrary \emph{tip} versions that
1.11 merely reflect snapshots that are never really up-to-date.} *}
1.12 @@ -37,7 +37,7 @@
1.13 certain style of writing Isabelle/ML that has emerged from long
1.14 years of system development.\footnote{See also the interesting style
1.15 guide for OCaml
1.16 - \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}
1.17 + @{url "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"}
1.18 which shares many of our means and ends.}
1.19
1.20 The main principle behind any coding style is \emph{consistency}.
2.1 --- a/src/Doc/JEdit/JEdit.thy Mon Dec 09 12:16:52 2013 +0100
2.2 +++ b/src/Doc/JEdit/JEdit.thy Mon Dec 09 12:22:23 2013 +0100
2.3 @@ -41,9 +41,9 @@
2.4 between ML and Scala, using asynchronous protocol commands.
2.5
2.6 \item [jEdit] is a sophisticated text editor implemented in
2.7 - Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
2.8 + Java.\footnote{@{url "http://www.jedit.org"}} It is easily extensible
2.9 by plugins written in languages that work on the JVM, e.g.\
2.10 - Scala\footnote{\url{http://www.scala-lang.org/}}.
2.11 + Scala\footnote{@{url "http://www.scala-lang.org/"}}.
2.12
2.13 \item [Isabelle/jEdit] is the main example application of the PIDE
2.14 framework and the default user-interface for Isabelle. It targets
2.15 @@ -74,7 +74,7 @@
2.16
2.17 Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
2.18 plugins for the well-known jEdit text editor
2.19 - \url{http://www.jedit.org}, according to the following principles.
2.20 + @{url "http://www.jedit.org"}, according to the following principles.
2.21
2.22 \begin{itemize}
2.23
2.24 @@ -125,7 +125,7 @@
2.25 full \emph{User's Guide} and \emph{Frequently Asked Questions} for
2.26 this sophisticated text editor. The same can be browsed without the
2.27 technical restrictions of the built-in Java HTML viewer here:
2.28 - \url{http://www.jedit.org/index.php?page=docs} (potentially for a
2.29 + @{url "http://www.jedit.org/index.php?page=docs"} (potentially for a
2.30 different version of jEdit).
2.31
2.32 Most of this information about jEdit is relevant for Isabelle/jEdit
3.1 --- a/src/Doc/Locales/Examples3.thy Mon Dec 09 12:16:52 2013 +0100
3.2 +++ b/src/Doc/Locales/Examples3.thy Mon Dec 09 12:22:23 2013 +0100
3.3 @@ -531,7 +531,7 @@
3.4
3.5 The sources of this tutorial, which include all proofs, are
3.6 available with the Isabelle distribution at
3.7 - \url{http://isabelle.in.tum.de}.
3.8 + @{url "http://isabelle.in.tum.de"}.
3.9 *}
3.10
3.11 text {*
4.1 --- a/src/Doc/Main/Main_Doc.thy Mon Dec 09 12:16:52 2013 +0100
4.2 +++ b/src/Doc/Main/Main_Doc.thy Mon Dec 09 12:22:23 2013 +0100
4.3 @@ -26,7 +26,7 @@
4.4 text{*
4.5
4.6 \begin{abstract}
4.7 -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/}.
4.8 +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/"}.
4.9 \end{abstract}
4.10
4.11 \section*{HOL}
5.1 --- a/src/Doc/ProgProve/Basics.thy Mon Dec 09 12:16:52 2013 +0100
5.2 +++ b/src/Doc/ProgProve/Basics.thy Mon Dec 09 12:22:23 2013 +0100
5.3 @@ -124,9 +124,9 @@
5.4 \end{warn}
5.5
5.6 In addition to the theories that come with the Isabelle/HOL distribution
5.7 -(see \url{http://isabelle.in.tum.de/library/HOL/})
5.8 +(see @{url "http://isabelle.in.tum.de/library/HOL/"})
5.9 there is also the \emph{Archive of Formal Proofs}
5.10 -at \url{http://afp.sourceforge.net}, a growing collection of Isabelle theories
5.11 +at @{url "http://afp.sourceforge.net"}, a growing collection of Isabelle theories
5.12 that everybody can contribute to.
5.13
5.14 \subsection{Quotation Marks}
6.1 --- a/src/Doc/System/Interfaces.thy Mon Dec 09 12:16:52 2013 +0100
6.2 +++ b/src/Doc/System/Interfaces.thy Mon Dec 09 12:22:23 2013 +0100
6.3 @@ -7,7 +7,7 @@
6.4 section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
6.5
6.6 text {* The @{tool_def jedit} tool invokes a version of
6.7 - jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
6.8 + jEdit\footnote{@{url "http://www.jedit.org/"}} that has been augmented
6.9 with some plugins to provide a fully-featured Prover IDE:
6.10 \begin{ttbox} Usage: isabelle jedit [OPTIONS]
6.11 [FILES ...]
6.12 @@ -49,7 +49,7 @@
6.13 self-build mechanism of Isabelle/jEdit. This is only relevant for
6.14 building from sources, which also requires an auxiliary @{verbatim
6.15 jedit_build}
6.16 - component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
6.17 + component.\footnote{@{url "http://isabelle.in.tum.de/components"}} Note
6.18 that official Isabelle releases already include a version of
6.19 Isabelle/jEdit that is built properly.
6.20 *}
6.21 @@ -58,7 +58,7 @@
6.22 section {* Proof General / Emacs *}
6.23
6.24 text {* The @{tool_def emacs} tool invokes a version of Emacs and
6.25 - Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
6.26 + Proof General\footnote{@{url "http://proofgeneral.inf.ed.ac.uk/"}} within the
6.27 regular Isabelle settings environment (\secref{sec:settings}). This
6.28 is more convenient than starting Emacs separately, loading the Proof
6.29 General LISP files, and then attempting to start Isabelle with
7.1 --- a/src/Doc/System/Misc.thy Mon Dec 09 12:16:52 2013 +0100
7.2 +++ b/src/Doc/System/Misc.thy Mon Dec 09 12:22:23 2013 +0100
7.3 @@ -34,7 +34,7 @@
7.4 in a permissive manner, which can mark components as ``missing''.
7.5 This state is amended by letting @{tool "components"} download and
7.6 unpack components that are published on the default component
7.7 - repository \url{http://isabelle.in.tum.de/components/} in
7.8 + repository @{url "http://isabelle.in.tum.de/components/"} in
7.9 particular.
7.10
7.11 Option @{verbatim "-R"} specifies an alternative component
8.1 --- a/src/Doc/System/Sessions.thy Mon Dec 09 12:16:52 2013 +0100
8.2 +++ b/src/Doc/System/Sessions.thy Mon Dec 09 12:22:23 2013 +0100
8.3 @@ -139,7 +139,7 @@
8.4 quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},
8.5 @{text "HOL\<dash>SPARK\<dash>Examples"}. An alternative is to use
8.6 unqualified names that are relatively long and descriptive, as in
8.7 - the Archive of Formal Proofs (\url{http://afp.sf.net}), for
8.8 + the Archive of Formal Proofs (@{url "http://afp.sf.net"}), for
8.9 example. *}
8.10
8.11
9.1 --- a/src/HOL/Bali/Decl.thy Mon Dec 09 12:16:52 2013 +0100
9.2 +++ b/src/HOL/Bali/Decl.thy Mon Dec 09 12:22:23 2013 +0100
9.3 @@ -15,7 +15,7 @@
9.4 \item clarification and correction of some aspects of the package/access concept
9.5 (Also submitted as bug report to the Java Bug Database:
9.6 Bug Id: 4485402 and Bug Id: 4493343
9.7 - http://developer.java.sun.com/developer/bugParade/index.jshtml
9.8 + @{url "http://developer.java.sun.com/developer/bugParade/index.jshtml"}
9.9 )
9.10 \end{itemize}
9.11 simplifications:
10.1 --- a/src/HOL/Groups.thy Mon Dec 09 12:16:52 2013 +0100
10.2 +++ b/src/HOL/Groups.thy Mon Dec 09 12:22:23 2013 +0100
10.3 @@ -567,7 +567,7 @@
10.4 \end{itemize}
10.5 Most of the used notions can also be looked up in
10.6 \begin{itemize}
10.7 - \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
10.8 + \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
10.9 \item \emph{Algebra I} by van der Waerden, Springer.
10.10 \end{itemize}
10.11 *}
11.1 --- a/src/HOL/Imperative_HOL/Ref.thy Mon Dec 09 12:16:52 2013 +0100
11.2 +++ b/src/HOL/Imperative_HOL/Ref.thy Mon Dec 09 12:22:23 2013 +0100
11.3 @@ -10,8 +10,8 @@
11.4
11.5 text {*
11.6 Imperative reference operations; modeled after their ML counterparts.
11.7 - See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
11.8 - and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
11.9 + See @{url "http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html"}
11.10 + and @{url "http://www.smlnj.org/doc/Conversion/top-level-comparison.html"}
11.11 *}
11.12
11.13 subsection {* Primitives *}
12.1 --- a/src/HOL/Induct/Ordinals.thy Mon Dec 09 12:16:52 2013 +0100
12.2 +++ b/src/HOL/Induct/Ordinals.thy Mon Dec 09 12:22:23 2013 +0100
12.3 @@ -11,7 +11,7 @@
12.4 text {*
12.5 Some basic definitions of ordinal numbers. Draws an Agda
12.6 development (in Martin-L\"of type theory) by Peter Hancock (see
12.7 - \url{http://www.dcs.ed.ac.uk/home/pgh/chat.html}).
12.8 + @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
12.9 *}
12.10
12.11 datatype ordinal =
13.1 --- a/src/HOL/Library/Binomial.thy Mon Dec 09 12:16:52 2013 +0100
13.2 +++ b/src/HOL/Library/Binomial.thy Mon Dec 09 12:22:23 2013 +0100
13.3 @@ -186,7 +186,7 @@
13.4
13.5 subsection{* Pochhammer's symbol : generalized rising factorial *}
13.6
13.7 -text {* See \url{http://en.wikipedia.org/wiki/Pochhammer_symbol} *}
13.8 +text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
13.9
13.10 definition "pochhammer (a::'a::comm_semiring_1) n =
13.11 (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
14.1 --- a/src/HOL/Library/Kleene_Algebra.thy Mon Dec 09 12:16:52 2013 +0100
14.2 +++ b/src/HOL/Library/Kleene_Algebra.thy Mon Dec 09 12:22:23 2013 +0100
14.3 @@ -14,7 +14,7 @@
14.4 text {* Various lemmas correspond to entries in a database of theorems
14.5 about Kleene algebras and related structures maintained by Peter
14.6 H\"ofner: see
14.7 - \url{http://www.informatik.uni-augsburg.de/~hoefnepe/kleene_db/lemmas/index.html}. *}
14.8 + @{url "http://www.informatik.uni-augsburg.de/~hoefnepe/kleene_db/lemmas/index.html"}. *}
14.9
14.10 subsection {* Preliminaries *}
14.11
15.1 --- a/src/HOL/Library/State_Monad.thy Mon Dec 09 12:16:52 2013 +0100
15.2 +++ b/src/HOL/Library/State_Monad.thy Mon Dec 09 12:22:23 2013 +0100
15.3 @@ -20,7 +20,7 @@
15.4 monads}, since a state is transformed single-threadedly).
15.5
15.6 To enter from the Haskell world,
15.7 - \url{http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm} makes
15.8 + @{url "http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm"} makes
15.9 a good motivating start. Here we just sketch briefly how those
15.10 monads enter the game of Isabelle/HOL.
15.11 *}
16.1 --- a/src/HOL/Library/Sum_of_Squares.thy Mon Dec 09 12:16:52 2013 +0100
16.2 +++ b/src/HOL/Library/Sum_of_Squares.thy Mon Dec 09 12:22:23 2013 +0100
16.3 @@ -24,7 +24,7 @@
16.4 \item local solver: @{text "(sos csdp)"}
16.5
16.6 The latter requires a local executable from
16.7 - https://projects.coin-or.org/Csdp and the Isabelle settings variable
16.8 + @{url "https://projects.coin-or.org/Csdp"} and the Isabelle settings variable
16.9 variable @{text ISABELLE_CSDP} pointing to it.
16.10
16.11 \end{itemize}
17.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Dec 09 12:16:52 2013 +0100
17.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Dec 09 12:22:23 2013 +0100
17.3 @@ -410,7 +410,7 @@
17.4
17.5 text {* TODO: The following lemmas about adjoints should hold for any
17.6 Hilbert space (i.e. complete inner product space).
17.7 -(see \url{http://en.wikipedia.org/wiki/Hermitian_adjoint})
17.8 +(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
17.9 *}
17.10
17.11 lemma adjoint_works:
18.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Dec 09 12:16:52 2013 +0100
18.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Dec 09 12:22:23 2013 +0100
18.3 @@ -16,8 +16,8 @@
18.4 by Roshan James (Indiana University) and also by the lecture notes
18.5 written by Andy Pitts for his semantics course. See
18.6
18.7 - http://www.cs.indiana.edu/~rpjames/lm.pdf
18.8 - http://www.cl.cam.ac.uk/teaching/2001/Semantics/
18.9 + @{url "http://www.cs.indiana.edu/~rpjames/lm.pdf"}
18.10 + @{url "http://www.cl.cam.ac.uk/teaching/2001/Semantics/"}
18.11
18.12 *}
18.13
19.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Dec 09 12:16:52 2013 +0100
19.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Dec 09 12:22:23 2013 +0100
19.3 @@ -4,7 +4,7 @@
19.4 "~~/src/HOL/Library/Code_Prolog"
19.5 begin
19.6
19.7 -text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}
19.8 +text {* An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"}) *}
19.9 text {* The example (original in Haskell) was imported with Haskabelle and
19.10 manually slightly adapted.
19.11 *}
20.1 --- a/src/HOL/Real_Vector_Spaces.thy Mon Dec 09 12:16:52 2013 +0100
20.2 +++ b/src/HOL/Real_Vector_Spaces.thy Mon Dec 09 12:22:23 2013 +0100
20.3 @@ -1414,7 +1414,7 @@
20.4
20.5 text {*
20.6 Proof that Cauchy sequences converge based on the one from
20.7 -http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
20.8 +@{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
20.9 *}
20.10
20.11 text {*
21.1 --- a/src/HOL/Rings.thy Mon Dec 09 12:16:52 2013 +0100
21.2 +++ b/src/HOL/Rings.thy Mon Dec 09 12:22:23 2013 +0100
21.3 @@ -449,7 +449,7 @@
21.4 \end{itemize}
21.5 Most of the used notions can also be looked up in
21.6 \begin{itemize}
21.7 - \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
21.8 + \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
21.9 \item \emph{Algebra I} by van der Waerden, Springer.
21.10 \end{itemize}
21.11 *}
22.1 --- a/src/HOL/Series.thy Mon Dec 09 12:16:52 2013 +0100
22.2 +++ b/src/HOL/Series.thy Mon Dec 09 12:22:23 2013 +0100
22.3 @@ -719,8 +719,10 @@
22.4
22.5 subsection {* Cauchy Product Formula *}
22.6
22.7 -(* Proof based on Analysis WebNotes: Chapter 07, Class 41
22.8 -http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm *)
22.9 +text {*
22.10 + Proof based on Analysis WebNotes: Chapter 07, Class 41
22.11 + @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
22.12 +*}
22.13
22.14 lemma setsum_triangle_reindex:
22.15 fixes n :: nat
23.1 --- a/src/HOL/ex/ML.thy Mon Dec 09 12:16:52 2013 +0100
23.2 +++ b/src/HOL/ex/ML.thy Mon Dec 09 12:22:23 2013 +0100
23.3 @@ -76,7 +76,7 @@
23.4 ML "factorial 10000 div factorial 9999"
23.5
23.6 text {*
23.7 - See http://mathworld.wolfram.com/AckermannFunction.html
23.8 + See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}
23.9 *}
23.10
23.11 ML {*
24.1 --- a/src/HOL/ex/NatSum.thy Mon Dec 09 12:16:52 2013 +0100
24.2 +++ b/src/HOL/ex/NatSum.thy Mon Dec 09 12:22:23 2013 +0100
24.3 @@ -10,7 +10,7 @@
24.4 Summing natural numbers, squares, cubes, etc.
24.5
24.6 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
24.7 - \url{http://www.research.att.com/~njas/sequences/}.
24.8 + @{url "http://www.research.att.com/~njas/sequences/"}.
24.9 *}
24.10
24.11 lemmas [simp] =
25.1 --- a/src/HOL/ex/Sudoku.thy Mon Dec 09 12:16:52 2013 +0100
25.2 +++ b/src/HOL/ex/Sudoku.thy Mon Dec 09 12:22:23 2013 +0100
25.3 @@ -137,7 +137,7 @@
25.4
25.5 text {*
25.6 Some "exceptionally difficult" Sudokus, taken from
25.7 - \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}
25.8 + @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
25.9 (accessed December 2, 2008).
25.10 *}
25.11