remove MiniML and Lex (moved to AFP)
authorkleing
Mon, 12 Apr 2004 23:59:19 +0200
changeset 14543 0e266a5dd6e3
parent 14542 f4fa346a0b46
child 14544 2d0c4c5819d3
remove MiniML and Lex (moved to AFP)
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