# HG changeset patch # User wenzelm # Date 1247170399 -7200 # Node ID 366ad09d39ef9825080a14f7636d70d5d4bd50d1 # Parent e81979a703a4dd274001ae7fd7a84c952f5439c4 removed obsolete CVS Ids; diff -r e81979a703a4 -r 366ad09d39ef src/HOL/Library/Library/ROOT.ML --- 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"]; diff -r e81979a703a4 -r 366ad09d39ef src/HOL/Library/Library/document/root.tex --- 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} diff -r e81979a703a4 -r 366ad09d39ef src/HOL/Library/README.html --- 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 @@ - -