changeset 7626 | 5997f35954d7 |
child 9000 | c20d58286a51 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/ROOT.ML Tue Sep 28 16:36:12 1999 +0200 @@ -0,0 +1,12 @@ +(* 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";