(* Title: HOL/BCV/ROOT.ML ID: $Id$ Author: Tobias Nipkow Copyright 1999 TUM A simple model of dataflow (sub)type analysis of instruction sequences, aka `bytecode verification'. *) writeln"Root file for HOL/BCV"; time_use_thy "Machine";