# HG changeset patch
# User kleing
# Date 1081807159 -7200
# Node ID 0e266a5dd6e37e9d614efb0b00189e060bc80050
# Parent  f4fa346a0b465f234a568de83388b17ac9622212
remove MiniML and Lex (moved to AFP)

diff -r f4fa346a0b46 -r 0e266a5dd6e3 src/HOL/README.html
--- a/src/HOL/README.html	Mon Apr 12 23:53:53 2004 +0200
+++ b/src/HOL/README.html	Mon Apr 12 23:59:19 2004 +0200
@@ -64,17 +64,11 @@
 <dt>Lattice
 <dd>lattices and order structures (in Isabelle/Isar)
 
-<dt>Lex
-<dd>verification of a simple lexical analyser generator
-
 <dt>MicroJava
 <dd>formalization of a fragment of Java, together with a corresponding
 virtual machine and a specification of its bytecode verifier and a
 lightweight bytecode verifier, including proofs of type-safety.
 
-<dt>MiniML
-<dd>formalization of type inference for the language Mini-ML
-
 <dt>Modelcheck
 <dd>basic setup for integration of some model checkers in Isabelle/HOL