more antiquotations;
authorwenzelm
Mon Dec 09 12:22:23 2013 +0100 (2013-12-09)
changeset 54703499f92dc6e45
parent 54702 3daeba5130f0
child 54704 ea71549629e2
more antiquotations;
src/Doc/IsarImplementation/ML.thy
src/Doc/JEdit/JEdit.thy
src/Doc/Locales/Examples3.thy
src/Doc/Main/Main_Doc.thy
src/Doc/ProgProve/Basics.thy
src/Doc/System/Interfaces.thy
src/Doc/System/Misc.thy
src/Doc/System/Sessions.thy
src/HOL/Bali/Decl.thy
src/HOL/Groups.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Induct/Ordinals.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Kleene_Algebra.thy
src/HOL/Library/State_Monad.thy
src/HOL/Library/Sum_of_Squares.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Nominal/Examples/CK_Machine.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/Series.thy
src/HOL/ex/ML.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Sudoku.thy
     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