# HG changeset patch
# User wenzelm
# Date 1386588143 -3600
# Node ID 499f92dc6e45ae30f64a9d01d0fc4371b0a2d694
# Parent  3daeba5130f00564e81ebfe6d2877c0f00a7c6b6
more antiquotations;

diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/IsarImplementation/ML.thy
--- 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}.
diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/JEdit/JEdit.thy
--- 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
diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/Locales/Examples3.thy
--- 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 {*
diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/Main/Main_Doc.thy
--- 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}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/ProgProve/Basics.thy
--- 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}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/System/Interfaces.thy
--- 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
diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/System/Misc.thy
--- 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
diff -r 3daeba5130f0 -r 499f92dc6e45 src/Doc/System/Sessions.thy
--- 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. *}
 
 
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Bali/Decl.thy
--- 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:
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Groups.thy
--- 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}
 *}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Imperative_HOL/Ref.thy
--- 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 *}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Induct/Ordinals.thy
--- 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 =
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Library/Binomial.thy
--- 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})"
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Library/Kleene_Algebra.thy
--- 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 *}
 
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Library/State_Monad.thy
--- 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.
 *}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Library/Sum_of_Squares.thy
--- 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}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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:
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Nominal/Examples/CK_Machine.thy
--- 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/"}
 
 *}
 
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- 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.
 *}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Real_Vector_Spaces.thy
--- 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 {*
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Rings.thy
--- 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}
 *}
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Series.thy
--- 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
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/ex/ML.thy
--- 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 {*
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/ex/NatSum.thy
--- 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] =
diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/ex/Sudoku.thy
--- 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).
 *}