remove MiniML and Lex (moved to AFP)
authorkleing
Mon, 12 Apr 2004 23:59:19 +0200
changeset 145430e266a5dd6e3
parent 14542 f4fa346a0b46
child 14544 2d0c4c5819d3
remove MiniML and Lex (moved to AFP)
src/HOL/README.html
     1.1 --- a/src/HOL/README.html	Mon Apr 12 23:53:53 2004 +0200
     1.2 +++ b/src/HOL/README.html	Mon Apr 12 23:59:19 2004 +0200
     1.3 @@ -64,17 +64,11 @@
     1.4  <dt>Lattice
     1.5  <dd>lattices and order structures (in Isabelle/Isar)
     1.6  
     1.7 -<dt>Lex
     1.8 -<dd>verification of a simple lexical analyser generator
     1.9 -
    1.10  <dt>MicroJava
    1.11  <dd>formalization of a fragment of Java, together with a corresponding
    1.12  virtual machine and a specification of its bytecode verifier and a
    1.13  lightweight bytecode verifier, including proofs of type-safety.
    1.14  
    1.15 -<dt>MiniML
    1.16 -<dd>formalization of type inference for the language Mini-ML
    1.17 -
    1.18  <dt>Modelcheck
    1.19  <dd>basic setup for integration of some model checkers in Isabelle/HOL
    1.20