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 @@
Lattice
lattices and order structures (in Isabelle/Isar) -
Lex -
verification of a simple lexical analyser generator -
MicroJava
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. -
MiniML -
formalization of type inference for the language Mini-ML -
Modelcheck
basic setup for integration of some model checkers in Isabelle/HOL