src/HOLCF/IOA/ABP/ROOT.ML
author wenzelm
Wed Nov 11 14:15:11 2009 +0100 (2009-11-11)
changeset 33615 261abc2e3155
parent 26981 0e7ba2749d70
child 39119 7bfa17bcd5ee
permissions -rw-r--r--
uniform use of simultabeous use_thys;
haftmann@24584
     1
(*  Title:      HOLCF/IOA/ABP/ROOT.ML
kleing@19360
     2
    Author:     Olaf Mueller
mueller@3072
     3
wenzelm@4423
     4
This is the ROOT file for the Alternating Bit Protocol performed in
wenzelm@33615
     5
I/O-Automata.
wenzelm@33615
     6
*)
mueller@3072
     7
mueller@3072
     8
goals_limit := 1;
mueller@3072
     9
wenzelm@26981
    10
use "Check.ML";
wenzelm@33615
    11
use_thys ["Correctness"];