--- a/src/HOL/Algebra/README.html Tue Mar 12 21:59:48 2013 +0100
+++ b/src/HOL/Algebra/README.html Tue Mar 12 22:22:05 2013 +0100
@@ -110,9 +110,6 @@
<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
Author's <A HREF="http://www4.in.tum.de/~ballarin/publications.html">PhD thesis</A>, 1999.
-<HR>
-<P>Last modified on $Date$
-
<ADDRESS>
<P><A HREF="http://www4.in.tum.de/~ballarin">Clemens Ballarin</A>.
</ADDRESS>
--- a/src/HOL/Auth/Guard/README.html Tue Mar 12 21:59:48 2013 +0100
+++ b/src/HOL/Auth/Guard/README.html Tue Mar 12 22:22:05 2013 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- a/src/HOL/Auth/README.html Tue Mar 12 21:59:48 2013 +0100
+++ b/src/HOL/Auth/README.html Tue Mar 12 22:22:05 2013 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
@@ -46,9 +44,6 @@
<P>Frederic Blanqui has contributed a theory of guardedness, which is
demonstrated by proofs of some roving agent protocols.
-<HR>
-<P>Last modified $Date$
-
<ADDRESS>
<A
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
--- a/src/HOL/TLA/README.html Tue Mar 12 21:59:48 2013 +0100
+++ b/src/HOL/TLA/README.html Tue Mar 12 22:22:05 2013 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
--- a/src/HOL/UNITY/Comp/README.html Tue Mar 12 21:59:48 2013 +0100
+++ b/src/HOL/UNITY/Comp/README.html Tue Mar 12 22:22:05 2013 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
@@ -40,9 +38,6 @@
level of automation appears to be about the same as in HOL-UNITY by Flemming
Andersen et al.
-<HR>
-<P>Last modified on $Date$
-
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
--- a/src/HOL/UNITY/README.html Tue Mar 12 21:59:48 2013 +0100
+++ b/src/HOL/UNITY/README.html Tue Mar 12 22:22:05 2013 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
@@ -45,9 +43,6 @@
The directory <A HREF="Comp/"><CODE>Comp</CODE></A>
presents examples of proofs involving program composition.
-<HR>
-<P>Last modified on $Date$
-
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
--- a/src/HOL/UNITY/Simple/README.html Tue Mar 12 21:59:48 2013 +0100
+++ b/src/HOL/UNITY/Simple/README.html Tue Mar 12 22:22:05 2013 +0100
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<HTML>
<HEAD>
@@ -37,9 +35,6 @@
<A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)
</UL>
-<HR>
-<P>Last modified on $Date$
-
<ADDRESS>
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>