# HG changeset patch
# User wenzelm
# Date 1291306834 -3600
# Node ID be44a567ed28391eb519329f155b1d2e4c5cd618
# Parent  ca132ef449440ab0a97a2613065315b9a173cfcf
more antiquotations;
removed some slightly outdated text;

diff -r ca132ef44944 -r be44a567ed28 src/HOL/Isar_Examples/Hoare.thy
--- 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
diff -r ca132ef44944 -r be44a567ed28 src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- 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 *}
 
diff -r ca132ef44944 -r be44a567ed28 src/HOL/Isar_Examples/Summation.thy
--- 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.