diff --git a/thys/MiniML/README.html b/thys/MiniML/README.html
deleted file mode 100644
--- a/thys/MiniML/README.html
+++ /dev/null
@@ -1,18 +0,0 @@
-HOL/MiniML/README
-
-
-Type Inference for MiniML
-
-This theory defines the type inference rules and the type inference algorithm
-W for MiniML (simply-typed lambda terms with let) due to
-Milner. It proves the soundness and completeness of W w.r.t. the
-rules.
-
-
-
-A report describing the theory is found here:
-
-Type Inference Verified: Algorithm W in Isabelle/HOL.
-
-
-