removed obsolete CVS Ids;
authorwenzelm
Thu, 09 Jul 2009 22:13:19 +0200
changeset 31975 366ad09d39ef
parent 31974 e81979a703a4
child 31976 17414e2736f4
removed obsolete CVS Ids;
src/HOL/Library/Library/ROOT.ML
src/HOL/Library/Library/document/root.tex
src/HOL/Library/README.html
--- 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>