--- a/src/HOL/Isar_examples/README.html Tue Oct 20 19:36:52 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<!-- $Id$ -->
-
-<html>
-
-<head>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <title>HOL/Isar_examples</title>
-</head>
-
-<body>
-<h1>HOL/Isar_examples</h1>
-
-Isar offers a new high-level proof (and theory) language interface to
-Isabelle. This directory contains some example Isar documents. See
-also the included document, or the <a
-href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a> for more
-information.
-</body>
-</html>