--- a/src/HOL/Library/Library/ROOT.ML Thu Jul 09 22:09:58 2009 +0200
+++ b/src/HOL/Library/Library/ROOT.ML Thu Jul 09 22:13:19 2009 +0200
@@ -1,3 +1,1 @@
-(* $Id$ *)
-
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
--- a/src/HOL/Library/Library/document/root.tex Thu Jul 09 22:09:58 2009 +0200
+++ b/src/HOL/Library/Library/document/root.tex Thu Jul 09 22:13:19 2009 +0200
@@ -1,6 +1,3 @@
-
-% $Id$
-
\documentclass[11pt,a4paper]{article}
\usepackage{ifthen}
\usepackage[latin1]{inputenc}
--- a/src/HOL/Library/README.html Thu Jul 09 22:09:58 2009 +0200
+++ b/src/HOL/Library/README.html Thu Jul 09 22:13:19 2009 +0200
@@ -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>