1.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Thu Dec 02 16:52:52 2010 +0100
     1.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Thu Dec 02 17:20:34 2010 +0100
     1.3 @@ -16,8 +16,7 @@
     1.4  text {* The following abstract syntax and semantics of Hoare Logic
     1.5    over \texttt{WHILE} programs closely follows the existing tradition
     1.6    in Isabelle/HOL of formalizing the presentation given in
     1.7 -  \cite[\S6]{Winskel:1993}.  See also
     1.8 -  \url{http://isabelle.in.tum.de/library/Hoare/} and
     1.9 +  \cite[\S6]{Winskel:1993}.  See also @{file "~~/src/HOL/Hoare"} and
    1.10    \cite{Nipkow:1998:Winskel}. *}
    1.11  
    1.12  types
    1.13 @@ -364,7 +363,7 @@
    1.14  
    1.15  text {* We now load the \emph{original} ML file for proof scripts and
    1.16    tactic definition for the Hoare Verification Condition Generator
    1.17 -  (see \url{http://isabelle.in.tum.de/library/Hoare/}).  As far as we
    1.18 +  (see @{file "~~/src/HOL/Hoare/"}).  As far as we
    1.19    are concerned here, the result is a proof method \name{hoare}, which
    1.20    may be applied to a Hoare Logic assertion to extract purely logical
    1.21    verification conditions.  It is important to note that the method

     2.1 --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Dec 02 16:52:52 2010 +0100
     2.2 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Dec 02 17:20:34 2010 +0100
     2.3 @@ -10,9 +10,7 @@
     2.4  begin
     2.5  
     2.6  text {* The Mutilated Checker Board Problem, formalized inductively.
     2.7 -  See \cite{paulson-mutilated-board} and
     2.8 -  \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for
     2.9 -  the original tactic script version. *}
    2.10 +  See \cite{paulson-mutilated-board} for the original tactic script version. *}
    2.11  
    2.12  subsection {* Tilings *}
    2.13  

     3.1 --- a/src/HOL/Isar_Examples/Summation.thy	Thu Dec 02 16:52:52 2010 +0100
     3.2 +++ b/src/HOL/Isar_Examples/Summation.thy	Thu Dec 02 17:20:34 2010 +0100
     3.3 @@ -8,11 +8,6 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -text_raw {* \footnote{This example is somewhat reminiscent of the
     3.8 -  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
     3.9 -  discussed in \cite{isabelle-ref} in the context of permutative
    3.10 -  rewrite rules and ordered rewriting.} *}
    3.11 -
    3.12  text {* Subsequently, we prove some summation laws of natural numbers
    3.13    (including odds, squares, and cubes).  These examples demonstrate
    3.14    how plain natural deduction (including induction) may be combined
    3.15 @@ -126,8 +121,8 @@
    3.16  qed
    3.17  
    3.18  text {* Comparing these examples with the tactic script version
    3.19 -  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
    3.20 -  an important difference of how induction vs.\ simplification is
    3.21 +  @{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference
    3.22 +  of how induction vs.\ simplification is
    3.23    applied.  While \cite[\S10]{isabelle-ref} advises for these examples
    3.24    that ``induction should not be applied until the goal is in the
    3.25    simplest form'' this would be a very bad idea in our setting.