src/HOL/BCV/ROOT.ML

new-style infix declaration for "image"

(*  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";