src/HOL/BCV/ROOT.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 7626 5997f35954d7
child 9791 a39e5d43de55
permissions -rw-r--r--
cleaned up;
nipkow@7626
     1
(*  Title:      HOL/BCV/ROOT.ML
nipkow@7626
     2
    ID:         $Id$
nipkow@7626
     3
    Author:     Tobias Nipkow
nipkow@7626
     4
    Copyright   1999 TUM
nipkow@7626
     5
nipkow@7626
     6
A simple model of dataflow (sub)type analysis of instruction sequences,
nipkow@7626
     7
aka `bytecode verification'.
nipkow@7626
     8
*)
nipkow@7626
     9
nipkow@7626
    10
time_use_thy "Machine";