removed obsolete CVS Ids;
authorwenzelm
Thu Jul 09 22:13:19 2009 +0200 (2009-07-09)
changeset 31975366ad09d39ef
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
     1.1 --- a/src/HOL/Library/Library/ROOT.ML	Thu Jul 09 22:09:58 2009 +0200
     1.2 +++ b/src/HOL/Library/Library/ROOT.ML	Thu Jul 09 22:13:19 2009 +0200
     1.3 @@ -1,3 +1,1 @@
     1.4 -(* $Id$ *)
     1.5 -
     1.6  use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
     2.1 --- a/src/HOL/Library/Library/document/root.tex	Thu Jul 09 22:09:58 2009 +0200
     2.2 +++ b/src/HOL/Library/Library/document/root.tex	Thu Jul 09 22:13:19 2009 +0200
     2.3 @@ -1,6 +1,3 @@
     2.4 -
     2.5 -% $Id$
     2.6 -
     2.7  \documentclass[11pt,a4paper]{article}
     2.8  \usepackage{ifthen}
     2.9  \usepackage[latin1]{inputenc}
     3.1 --- a/src/HOL/Library/README.html	Thu Jul 09 22:09:58 2009 +0200
     3.2 +++ b/src/HOL/Library/README.html	Thu Jul 09 22:13:19 2009 +0200
     3.3 @@ -1,7 +1,5 @@
     3.4  <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     3.5  
     3.6 -<!-- $Id$ -->
     3.7 -
     3.8  <html>
     3.9  
    3.10  <head>