--- a/src/HOL/Isar_Examples/Hoare.thy Thu Dec 02 16:52:52 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Thu Dec 02 17:20:34 2010 +0100
@@ -16,8 +16,7 @@
text {* The following abstract syntax and semantics of Hoare Logic
over \texttt{WHILE} programs closely follows the existing tradition
in Isabelle/HOL of formalizing the presentation given in
- \cite[\S6]{Winskel:1993}. See also
- \url{http://isabelle.in.tum.de/library/Hoare/} and
+ \cite[\S6]{Winskel:1993}. See also @{file "~~/src/HOL/Hoare"} and
\cite{Nipkow:1998:Winskel}. *}
types
@@ -364,7 +363,7 @@
text {* We now load the \emph{original} ML file for proof scripts and
tactic definition for the Hoare Verification Condition Generator
- (see \url{http://isabelle.in.tum.de/library/Hoare/}). As far as we
+ (see @{file "~~/src/HOL/Hoare/"}). As far as we
are concerned here, the result is a proof method \name{hoare}, which
may be applied to a Hoare Logic assertion to extract purely logical
verification conditions. It is important to note that the method
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Dec 02 16:52:52 2010 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Thu Dec 02 17:20:34 2010 +0100
@@ -10,9 +10,7 @@
begin
text {* The Mutilated Checker Board Problem, formalized inductively.
- See \cite{paulson-mutilated-board} and
- \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for
- the original tactic script version. *}
+ See \cite{paulson-mutilated-board} for the original tactic script version. *}
subsection {* Tilings *}
--- a/src/HOL/Isar_Examples/Summation.thy Thu Dec 02 16:52:52 2010 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy Thu Dec 02 17:20:34 2010 +0100
@@ -8,11 +8,6 @@
imports Main
begin
-text_raw {* \footnote{This example is somewhat reminiscent of the
- \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
- discussed in \cite{isabelle-ref} in the context of permutative
- rewrite rules and ordered rewriting.} *}
-
text {* Subsequently, we prove some summation laws of natural numbers
(including odds, squares, and cubes). These examples demonstrate
how plain natural deduction (including induction) may be combined
@@ -126,8 +121,8 @@
qed
text {* Comparing these examples with the tactic script version
- \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
- an important difference of how induction vs.\ simplification is
+ @{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference
+ of how induction vs.\ simplification is
applied. While \cite[\S10]{isabelle-ref} advises for these examples
that ``induction should not be applied until the goal is in the
simplest form'' this would be a very bad idea in our setting.