src/HOL/BCV/ROOT.ML

Completely new version of BCV

(*  Title:      HOL/BCV/ROOT.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TUM

A simple model of dataflow (sub)type analysis of instruction sequences,
aka `bytecode verification'.
*)

writeln"Root file for HOL/BCV";

use_thy"JVM";