changeset 15582 | 7219facb3fd0 |
parent 15283 | f21466450330 |
child 26406 | be5b78d95801 |
--- a/src/HOL/Library/README.html Mon Mar 07 18:40:36 2005 +0100 +++ b/src/HOL/Library/README.html Mon Mar 07 19:17:07 2005 +0100 @@ -1,10 +1,13 @@ <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> +<!-- $Id$ --> + <html> -<!-- $Id$ --> - -<head><title>HOL-Library/README</title></head> +<head> + <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> + <title>HOL-Library/README</title> +</head> <body>