--- a/src/Doc/IsarImplementation/ML.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Mon Dec 09 12:22:23 2013 +0100
@@ -22,7 +22,7 @@
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{See
- \url{http://isabelle.in.tum.de/repos/isabelle} for the full
+ @{url "http://isabelle.in.tum.de/repos/isabelle"} for the full
Mercurial history. There are symbolic tags to refer to official
Isabelle releases, as opposed to arbitrary \emph{tip} versions that
merely reflect snapshots that are never really up-to-date.} *}
@@ -37,7 +37,7 @@
certain style of writing Isabelle/ML that has emerged from long
years of system development.\footnote{See also the interesting style
guide for OCaml
- \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}
+ @{url "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"}
which shares many of our means and ends.}
The main principle behind any coding style is \emph{consistency}.
--- a/src/Doc/JEdit/JEdit.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Dec 09 12:22:23 2013 +0100
@@ -41,9 +41,9 @@
between ML and Scala, using asynchronous protocol commands.
\item [jEdit] is a sophisticated text editor implemented in
- Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
+ Java.\footnote{@{url "http://www.jedit.org"}} It is easily extensible
by plugins written in languages that work on the JVM, e.g.\
- Scala\footnote{\url{http://www.scala-lang.org/}}.
+ Scala\footnote{@{url "http://www.scala-lang.org/"}}.
\item [Isabelle/jEdit] is the main example application of the PIDE
framework and the default user-interface for Isabelle. It targets
@@ -74,7 +74,7 @@
Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
plugins for the well-known jEdit text editor
- \url{http://www.jedit.org}, according to the following principles.
+ @{url "http://www.jedit.org"}, according to the following principles.
\begin{itemize}
@@ -125,7 +125,7 @@
full \emph{User's Guide} and \emph{Frequently Asked Questions} for
this sophisticated text editor. The same can be browsed without the
technical restrictions of the built-in Java HTML viewer here:
- \url{http://www.jedit.org/index.php?page=docs} (potentially for a
+ @{url "http://www.jedit.org/index.php?page=docs"} (potentially for a
different version of jEdit).
Most of this information about jEdit is relevant for Isabelle/jEdit
--- a/src/Doc/Locales/Examples3.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/Locales/Examples3.thy Mon Dec 09 12:22:23 2013 +0100
@@ -531,7 +531,7 @@
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
- \url{http://isabelle.in.tum.de}.
+ @{url "http://isabelle.in.tum.de"}.
*}
text {*
--- a/src/Doc/Main/Main_Doc.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/Main/Main_Doc.thy Mon Dec 09 12:22:23 2013 +0100
@@ -26,7 +26,7 @@
text{*
\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 "http://isabelle.in.tum.de/library/HOL/"}.
\end{abstract}
\section*{HOL}
--- a/src/Doc/ProgProve/Basics.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/ProgProve/Basics.thy Mon Dec 09 12:22:23 2013 +0100
@@ -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 "http://isabelle.in.tum.de/library/HOL/"})
there is also the \emph{Archive of Formal Proofs}
-at \url{http://afp.sourceforge.net}, a growing collection of Isabelle theories
+at @{url "http://afp.sourceforge.net"}, a growing collection of Isabelle theories
that everybody can contribute to.
\subsection{Quotation Marks}
--- a/src/Doc/System/Interfaces.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/System/Interfaces.thy Mon Dec 09 12:22:23 2013 +0100
@@ -7,7 +7,7 @@
section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
text {* The @{tool_def jedit} tool invokes a version of
- jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
+ jEdit\footnote{@{url "http://www.jedit.org/"}} that has been augmented
with some plugins to provide a fully-featured Prover IDE:
\begin{ttbox} Usage: isabelle jedit [OPTIONS]
[FILES ...]
@@ -49,7 +49,7 @@
self-build mechanism of Isabelle/jEdit. This is only relevant for
building from sources, which also requires an auxiliary @{verbatim
jedit_build}
- component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
+ component.\footnote{@{url "http://isabelle.in.tum.de/components"}} Note
that official Isabelle releases already include a version of
Isabelle/jEdit that is built properly.
*}
@@ -58,7 +58,7 @@
section {* Proof General / Emacs *}
text {* The @{tool_def emacs} tool invokes a version of Emacs and
- Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
+ Proof General\footnote{@{url "http://proofgeneral.inf.ed.ac.uk/"}} within the
regular Isabelle settings environment (\secref{sec:settings}). This
is more convenient than starting Emacs separately, loading the Proof
General LISP files, and then attempting to start Isabelle with
--- a/src/Doc/System/Misc.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/System/Misc.thy Mon Dec 09 12:22:23 2013 +0100
@@ -34,7 +34,7 @@
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
+ repository @{url "http://isabelle.in.tum.de/components/"} in
particular.
Option @{verbatim "-R"} specifies an alternative component
--- a/src/Doc/System/Sessions.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/Doc/System/Sessions.thy Mon Dec 09 12:22:23 2013 +0100
@@ -139,7 +139,7 @@
quasi-hierarchic naming conventions like @{text "HOL\<dash>SPARK"},
@{text "HOL\<dash>SPARK\<dash>Examples"}. An alternative is to use
unqualified names that are relatively long and descriptive, as in
- the Archive of Formal Proofs (\url{http://afp.sf.net}), for
+ the Archive of Formal Proofs (@{url "http://afp.sf.net"}), for
example. *}
--- a/src/HOL/Bali/Decl.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Bali/Decl.thy Mon Dec 09 12:22:23 2013 +0100
@@ -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
- http://developer.java.sun.com/developer/bugParade/index.jshtml
+ @{url "http://developer.java.sun.com/developer/bugParade/index.jshtml"}
)
\end{itemize}
simplifications:
--- a/src/HOL/Groups.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Groups.thy Mon Dec 09 12:22:23 2013 +0100
@@ -567,7 +567,7 @@
\end{itemize}
Most of the used notions can also be looked up in
\begin{itemize}
- \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
+ \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
\item \emph{Algebra I} by van der Waerden, Springer.
\end{itemize}
*}
--- a/src/HOL/Imperative_HOL/Ref.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Mon Dec 09 12:22:23 2013 +0100
@@ -10,8 +10,8 @@
text {*
Imperative reference operations; modeled after their ML counterparts.
- See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
- and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
+ 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"}
*}
subsection {* Primitives *}
--- a/src/HOL/Induct/Ordinals.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Induct/Ordinals.thy Mon Dec 09 12:22:23 2013 +0100
@@ -11,7 +11,7 @@
text {*
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 "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
*}
datatype ordinal =
--- a/src/HOL/Library/Binomial.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Library/Binomial.thy Mon Dec 09 12:22:23 2013 +0100
@@ -186,7 +186,7 @@
subsection{* Pochhammer's symbol : generalized rising factorial *}
-text {* See \url{http://en.wikipedia.org/wiki/Pochhammer_symbol} *}
+text {* See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"} *}
definition "pochhammer (a::'a::comm_semiring_1) n =
(if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
--- a/src/HOL/Library/Kleene_Algebra.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Library/Kleene_Algebra.thy Mon Dec 09 12:22:23 2013 +0100
@@ -14,7 +14,7 @@
text {* Various lemmas correspond to entries in a database of theorems
about Kleene algebras and related structures maintained by Peter
H\"ofner: see
- \url{http://www.informatik.uni-augsburg.de/~hoefnepe/kleene_db/lemmas/index.html}. *}
+ @{url "http://www.informatik.uni-augsburg.de/~hoefnepe/kleene_db/lemmas/index.html"}. *}
subsection {* Preliminaries *}
--- a/src/HOL/Library/State_Monad.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Library/State_Monad.thy Mon Dec 09 12:22:23 2013 +0100
@@ -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 "http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm"} makes
a good motivating start. Here we just sketch briefly how those
monads enter the game of Isabelle/HOL.
*}
--- a/src/HOL/Library/Sum_of_Squares.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Library/Sum_of_Squares.thy Mon Dec 09 12:22:23 2013 +0100
@@ -24,7 +24,7 @@
\item local solver: @{text "(sos csdp)"}
The latter requires a local executable from
- https://projects.coin-or.org/Csdp and the Isabelle settings variable
+ @{url "https://projects.coin-or.org/Csdp"} and the Isabelle settings variable
variable @{text ISABELLE_CSDP} pointing to it.
\end{itemize}
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Dec 09 12:22:23 2013 +0100
@@ -410,7 +410,7 @@
text {* 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})
+(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
*}
lemma adjoint_works:
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Mon Dec 09 12:22:23 2013 +0100
@@ -16,8 +16,8 @@
by Roshan James (Indiana University) and also by the lecture notes
written by Andy Pitts for his semantics course. See
- http://www.cs.indiana.edu/~rpjames/lm.pdf
- http://www.cl.cam.ac.uk/teaching/2001/Semantics/
+ @{url "http://www.cs.indiana.edu/~rpjames/lm.pdf"}
+ @{url "http://www.cl.cam.ac.uk/teaching/2001/Semantics/"}
*}
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Mon Dec 09 12:22:23 2013 +0100
@@ -4,7 +4,7 @@
"~~/src/HOL/Library/Code_Prolog"
begin
-text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}
+text {* An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"}) *}
text {* The example (original in Haskell) was imported with Haskabelle and
manually slightly adapted.
*}
--- a/src/HOL/Real_Vector_Spaces.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Dec 09 12:22:23 2013 +0100
@@ -1414,7 +1414,7 @@
text {*
Proof that Cauchy sequences converge based on the one from
-http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html
+@{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
*}
text {*
--- a/src/HOL/Rings.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Rings.thy Mon Dec 09 12:22:23 2013 +0100
@@ -449,7 +449,7 @@
\end{itemize}
Most of the used notions can also be looked up in
\begin{itemize}
- \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
+ \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
\item \emph{Algebra I} by van der Waerden, Springer.
\end{itemize}
*}
--- a/src/HOL/Series.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Series.thy Mon Dec 09 12:22:23 2013 +0100
@@ -719,8 +719,10 @@
subsection {* Cauchy Product Formula *}
-(* Proof based on Analysis WebNotes: Chapter 07, Class 41
-http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm *)
+text {*
+ Proof based on Analysis WebNotes: Chapter 07, Class 41
+ @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
+*}
lemma setsum_triangle_reindex:
fixes n :: nat
--- a/src/HOL/ex/ML.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/ex/ML.thy Mon Dec 09 12:22:23 2013 +0100
@@ -76,7 +76,7 @@
ML "factorial 10000 div factorial 9999"
text {*
- See http://mathworld.wolfram.com/AckermannFunction.html
+ See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}
*}
ML {*
--- a/src/HOL/ex/NatSum.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/ex/NatSum.thy Mon Dec 09 12:22:23 2013 +0100
@@ -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 "http://www.research.att.com/~njas/sequences/"}.
*}
lemmas [simp] =
--- a/src/HOL/ex/Sudoku.thy Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/ex/Sudoku.thy Mon Dec 09 12:22:23 2013 +0100
@@ -137,7 +137,7 @@
text {*
Some "exceptionally difficult" Sudokus, taken from
- \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}
+ @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
(accessed December 2, 2008).
*}